*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Curried functions in binding operators*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 16 Feb 2015 08:37:16 +0100*In-reply-to*: <54E06663.7030706@informatik.tu-muenchen.de>*References*: <54DC7840.3050100@inf.ethz.ch> <54E06663.7030706@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Dear Florian,

Andreas On 15/02/15 10:26, Florian Haftmann wrote:

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

**References**:**[isabelle] Curried functions in binding operators***From:*Andreas Lochbihler

**Re: [isabelle] Curried functions in binding operators***From:*Florian Haftmann

- Previous by Date: [isabelle] Generate PDF from .thy File?
- Next by Date: Re: [isabelle] Generate PDF from .thy File?
- Previous by Thread: Re: [isabelle] Curried functions in binding operators
- Next by Thread: [isabelle] Local_Theory.map_naming in locales
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list