[isabelle-dev] Let and tuple case expressions
Lawrence Paulson
lp15 at cam.ac.uk
Thu Oct 2 18:42:58 CEST 2014
Agree.
Larry
On 2 Oct 2014, at 17:13, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> In short, I have come to the conclusion that
>
> let (a, b) = p in t
>
> case p of (a, b) => t
>
> at the moment being logically distinct, should be one and the same.
>
> This is very much the same way as the code generator translates let- and
> case expression to target languages.
>
> Opinions?
More information about the isabelle-dev
mailing list