[isabelle-dev] Notes on datatype_new list

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon May 26 20:27:06 CEST 2014

Hi again,
> datatype_new 'a list =
> Nil (defaults un_Cons2: "[]") ("[]")
> | Cons 'a "'a list" (infixr "#" 65)
> abbreviation "map ≡ map_list"
> abbreviation "set ≡ set_list"
> abbreviation "list_all2 ≡ rel_list"
> abbreviation "hd ≡ un_Cons1"
> abbreviation "tl ≡ un_Cons2"

this would make sense if you were to abandon the lhses in favour of the
rhses in the mid future, which, as I dare to state plainly, you don't
want to do.  Duplication is a migration solution, not a solution in itself.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140526/e0af4f2e/attachment.sig>

More information about the isabelle-dev mailing list