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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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