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)))"
Quoting Christian Sternagel <christian.sternagel at uibk.ac.at>:
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