Hi all, 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 direction.
> 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
positional arguments:
> with
> 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
interpretation statements.
So far.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
