[isabelle-dev] Notes on datatype_new list
florian.haftmann at informatik.tu-muenchen.de
Mon May 26 20:22:41 CEST 2014
many issues have been touched in this thread, but I would like to get
back to the proposals made by Jasmin which IMHO point into the right
> 1. The squiggles (-: and =:) are easy to get rid of, and we'll kill
> them. This has been discussed before.
OK. No need to discuss this any longer.
> 2. We'll try to move (map: ... rel: ...) out of the way, e.g. by putting
> them after the definition rather than before.
This corresponds to the pattern »start with the main clause, put the
adverbial after«. Very good. In after-2007 Isar, there is also a
tendency to be more verbose in statements, avoiding too many implicit
> map := map_list
> set := set_list
> list_all2 := rel (* ugly name BTW -- maybe*)
instead of something like »(map set list_all2)«
> 3. Similar story for the set function (set: 'a), even though it's a bit
> painful in the general case (with, say, ten type variables and five
> mutually recursive types -- cf. IsaFoR).
Same argument: it is easier to understand a (natural language) sentence
if there are not too many interjections before the main predicate.
> 4. The selector syntax seems acceptable to most of not all parties. Some
> of us even love it. Also important is that readers are usually smart
> enough to infer, from the names of the things, what is meant (e.g. "hd"
> and "tl" for a list have to be the selectors).
I have no strong opinion about that. But the side discussion whether to
prefer »head« and »tail« seems also fruitful to avoid confusion.
> 5. The discriminators are a bit more iffy, and could perhaps be labeled
> more clearly, e.g. with a pseudo-keyword "discriminator". On the other
> hand, they're not needed for "list" and "option", and the default name
> (is_C for constructor C) is good.
I have a slight feeling that syntax for selectors and discriminators
should be corresponding.
> 6. The default values for, e.g. "tl  = ", could be specified as
> equations after the definition (e.g. in a "where" clause), as suggested
> one year ago by Andreas L.
This is more verbose to parse, but it also quite common in Isar to
require propostions of a certain shape instead of (conceptually
isomorphic) fragments. A similar example are mixin equations in
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev