[isabelle-dev] Let and tuple case expressions

[Tobias Nipkow]

Me too.

Tobias

On 02/10/2014 18:42, Lawrence Paulson wrote:
> 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?
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>