25 Jun
2008
25 Jun
'08
11:49 a.m.
Conal Elliott wrote:
I have a foggy memory that early ML had only binary pairing, nesting for n-tuples. Can anyone confirm this memory. If so, does anyone remember the rationale for going to n-tuples? Performance, perhaps?
In Isabelle HOL "*" is a right-associative (pair) type constructor. So "T1 * T2 * T3" is the same as "T1 * (T2 * T3)". Although the concept is minimal it is sort of asymmetric (wrt. associativity). Cheers Christian