Re: [isabelle] Curried functions in binding operators

> Here are my attempts so far:
> 1. apply(unfold split_def)
> This works but the resulting subgoal is
>   "g x Â= (Îy. f x Â= (Îx. h (fst (fst x)) (snd x) y)) = foo
> which is much harder to read than the desired
>   "g x Â= (Îy. f x Â= (Î((b, c), d). h b d y)) = foo"

I have never tried to tackle that issue, but a rough idea comes to my
mind: an optional simproc which collapses (%x. â fst x â snd x) to (%(a,
b). â a â b â).  No idea how this would work in practice.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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