Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



> On 17 Nov 2015, at 13:45, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 
> Incidentally, I'm tempted to rename "ctor" to "in" and "dtor" to "out", in keeping with some of the literature, to avoid any confusion between the actual high-level constructors (called "ctr"s in the code and some theorems) and the low-level constructors. If anybody is against this renaming, please speak out now.

I am against the renaming. Note that âinâ is a keyword in ML and you would need to start decorating the identifiers in the ML code with âxâ, âââ or â0â. Also in/out are much less symmetric than ctor/dtor. We have actual code that is parametric in the view (there the name xtor is used).

Dmitriy



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