>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>> =: Nil (defaults tl: "[]") ("[]")
>> | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
>> Can you explain the squiggle =: above? I did not find it in the manual
>> nor in the sources so far. It seems to be special to main HOL datatypes.
> what it does is indicate for Nil that a discriminator (of type "'a list =>
> bool")
> should not be provided, but instead equality with Nil should be used.
> This option seems to only be available for nullary constructors.
A couple more notes on this:
The places before the constructor names, like the one before Nil where "=:"
currently stands, can be used to give any discriminator name, as in
datatype_new (set: 'a) list (map: map rel: list_all2) =
myDiscriminatorForNil: Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
which yields myDiscriminatorForNil :: "'a list => bool" together with the
relevant facts.
The default is to generate a discriminator with name built from the
constructor, here is_Nil.
Note however that for lists a discriminator is_Cons is *not* generated unless
the user explicitly
requires one, since the datatype has only two constructors and it is more
convenient to use the negation
of is_Nil instead of is_Cons. However, if the datatype has more than two
constructors, as in
datatype_new (set: 'a) listBlah (map: map rel: list_all2) =
Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
| Blah
then discriminators are produced for all of them: is_Nil, is_Cons, and is_Blah.
Jasmin has polished these to the extreme.
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/datatypes.pdf
Andrei
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
