[isabelle-dev] Let and tuple case expressions

[Brian Huffman]

Perhaps this should be done uniformly for all single-constructor
datatypes, not just pairs. Any case expression with a single branch
could be printed as a "let".

- Brian

On Thu, Oct 2, 2014 at 9:13 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> In a private discussion, there had been a question what can be done against
>
>   let (a, b) = p in t
>
> being simplified by default to
>
>   case p of (a, b) => t
>
> I did one attempt (see attached patch) to suppress this.  However after
> realizing that proofs now tend to become more complicated, I spent a
> second thought on this.
>
> 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.  In
> other words, I suggest that any case expression on tuples should be
> printed using »let« rather than »case«.  The constant »Let« would turn
> into a degenerate case combinator with no actual pattern match.
>
> This is very much the same way as the code generator translates let- and
> case expression to target languages.
>
> Opinions?
>         Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>