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.haftm...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
