Re: [isabelle] Dealing with Cases
On Mon, 7 May 2012, Aaron W. Hsu wrote:
(case X of Blah x y => f x y)
= f (case X of Blah x y => x) (case X of Blah x y => y)
I guess that I am not sure how cases work under the hood, so I am not
sure how I would go about handling this, as splitting twice does not
seem to quite work the way that I want.
Just to understand the notation, you can use this in Isabelle2012 (e.g.
RC2) to disable the heavy sugar coating:
declare [[show_cases = false]]
This archive was generated by a fusion of
Pipermail (Mailman edition) and