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