[isabelle-dev] Let and tuple case expressions
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.
More information about the isabelle-dev