Re: [isabelle] Problem with Pairs

You can rewrite "(let (_,_,s) = f n in P s)" using
(simp only: Let_def split_def)

which results in "P (snd (snd (f n)))"

- Brian

Quoting Christian Sternagel <christian.sternagel at>:

Hi there,

I have problems using pattern-matching with pairs. The thing is that
I'm not able to prove equivalence between an expression

 (let (_,_,s) = f n in P s)


 P (snd (snd (f n)))

Are there any general advices (except, don't use pairing =)).



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.