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



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

We have clashes with many other names, e.g. "rec" (a keyword, or a recursor), "map", "fold" (ML functions one does not want to shadow), even "in"... (Grep "recx", "mapx", "foldx", "inx".) Such clashes, and their crude fix with an "x", are not pretty, but they are a reasonable price to pay for having the right names at the Isar level.

But there is in fact a possible confusion at the ML level, which is much worse than the inelegant "inx": "in" is already used in the code for set membership (\<in>), e.g.

    val inx = mk_in Asets sets T;

So maybe statu quo is best for now.

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

"in/out" are semantically very symmetric. I invented "xtor" out of sheer desperation and would happily trade it against "inout" or "io" or even "thru".

Jasmin





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