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