*To*: Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Tue, 17 Nov 2015 16:15:54 +0100*Cc*: Andrei Popescu <a.popescu at mdx.ac.uk>, Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <BA99CD80-8B07-4B98-AB75-D853024A7646@inf.ethz.ch>*References*: <564B1075.5060706@in.tum.de> <C67DA37B-EEE3-4BBD-9CEE-6AB41FF48ACE@inria.fr> <BA99CD80-8B07-4B98-AB75-D853024A7646@inf.ethz.ch>

> 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

**Follow-Ups**:**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Andrei Popescu

**References**:**[isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Isabelle as an interface to Z3
- Next by Date: Re: [isabelle] Failing afp-2015 build
- Previous by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list