[isabelle-dev] Let and tuple case expressions

Lawrence Paulson lp15 at cam.ac.uk
Thu Oct 2 18:42:58 CEST 2014


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