[isabelle-dev] Let and tuple case expressions
nipkow at in.tum.de
Thu Oct 2 18:51:49 CEST 2014
On 02/10/2014 18:42, Lawrence Paulson wrote:
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev