1val _ = new_theory "test";
2
3val _ = load_library_in_place (find_library "mutrec");
4
5structure test : MutRecTypeInputSig =
6struct
7
8structure TypeInfo = TypeInfo
9
10open TypeInfo
11
12val mut_rec_ty_spec =
13    [{type_name = "toto",
14      constructors=[{name ="empty_test", arg_info=[]}]}]
15val New_Ty_Existence_Thm_Name = "toto_existence_thm"
16val New_Ty_Induct_Thm_Name = "toto_induction_thm"
17val New_Ty_Uniqueness_Thm_Name = "toto_uniqueness_thm"
18val Constructors_One_One_Thm_Name = "toto_constructors_one_one"
19val Constructors_Distinct_Thm_Name = "toto_constructors_distinct"
20val Cases_Thm_Name = "toto_cases"
21
22end; (* struct *)
23
24structure test_Def = MutRecTypeFunc (test);
25
26
27
28structure test1 : MutRecTypeInputSig =
29struct
30
31structure TypeInfo = TypeInfo
32
33open TypeInfo
34
35val mut_rec_ty_spec =
36    [{type_name = "toto1",
37      constructors=[{name ="test1", arg_info=[existing(==`:'a`==)]},
38                    {name ="test2", arg_info=[existing(==`:'b`==)]}]},
39     {type_name = "tutu1",
40      constructors=[{name ="test3", arg_info=[]}]}]
41val New_Ty_Existence_Thm_Name = "toto1_existence_thm"
42val New_Ty_Induct_Thm_Name = "toto1_induction_thm"
43val New_Ty_Uniqueness_Thm_Name = "toto1_uniqueness_thm"
44val Constructors_Distinct_Thm_Name = "toto1_constructors_distinct"
45val Constructors_One_One_Thm_Name = "toto1_constructors_one_one"
46val Cases_Thm_Name = "toto1_cases"
47
48end; (* struct *)
49
50
51structure test1_Def = MutRecTypeFunc (test1);
52