Re: [isabelle] case split on tuples

On Mon, 27 Jun 2011, Christian Sternagel wrote:

recently I noticed that when using cases on right-nested tuples in Isar, I obtain just a single case (by the name "fields"), which is very
convenient. E.g.,

I started to rely on this behavior and used an ever deeper nesting of tuples... until (starting with 8 components) it didn't work any longer. What is the reason that at most 7 components are split?

The setup in src/HOL/Product_Type.thy assumes that tuples have max. 7 fields, see prod_cases7 etc. When I introduced that any years ago, the reasoning was that with many fields it is better to use records anyway.

The scala library has similar treatment for tuples of "reasonable size", where they define it as <= 22 fields.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.