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
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