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 uibk.ac.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)

and

 P (snd (snd (f n)))

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

cheers

christian








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