1open HolKernel Parse boolLib
2
3open Datatype
4
5val _ = new_theory "loadDatatypeA";
6
7val _ = Datatype`enum = EC1 | EC2 | EC3 | EC4`;
8
9val _ = Datatype`simple = SC1 num | SC2 bool num`
10
11val _ = Datatype`polysimple = PS1 'a | PS2 'b num`
12
13val _ = Datatype`recursive = RC1 num | RC2 recursive bool`
14
15val _ = Datatype`polyrec = PR1 'a | PR2 polyrec 'b`;
16
17val _ = Datatype`simpleref = SR1 num | SR2 ((num,'a) polyrec)`
18
19val _ = Datatype`
20  mut1 = con1 'a num | con2 mut2 ;
21  mut2 = con3 bool | con4 mut1 mut2
22`;
23
24val _ = Datatype`simplenest = SN1 num | SN2 (simplenest option)`;
25
26(* bug in older implementations of Datatype too --
27val _ = Datatype`
28  nested1 = con5 'a nested2 ;
29  nested2 = con6 (nested1 mut1)
30`;
31*)
32
33
34val _ = export_theory();
35