equal
deleted
inserted
replaced
75 let fun r i = proj (Bound 0) eqs i; |
75 let fun r i = proj (Bound 0) eqs i; |
76 in |
76 in |
77 ("copy_def", %%:(dname^"_copy") == /\ "f" |
77 ("copy_def", %%:(dname^"_copy") == /\ "f" |
78 (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) |
78 (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) |
79 end; |
79 end; |
80 |
|
81 val mat_defs = |
|
82 let |
|
83 fun mdef (con, _, _) = |
|
84 let |
|
85 val k = Bound 0 |
|
86 val x = Bound 1 |
|
87 fun one_con (con', _, args') = |
|
88 if con'=con then k else List.foldr /\# mk_fail args' |
|
89 val w = list_ccomb(%%:(dname^"_when"), map one_con cons) |
|
90 val rhs = /\ "x" (/\ "k" (w ` x)) |
|
91 in (mat_name con ^"_def", %%:(mat_name con) == rhs) end |
|
92 in map mdef cons end; |
|
93 |
80 |
94 val pat_defs = |
81 val pat_defs = |
95 let |
82 let |
96 fun pdef (con, _, args) = |
83 fun pdef (con, _, args) = |
97 let |
84 let |
123 mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
110 mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
124 |
111 |
125 in (dnam, |
112 in (dnam, |
126 (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), |
113 (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), |
127 (if definitional then [when_def] else [when_def, copy_def]) @ |
114 (if definitional then [when_def] else [when_def, copy_def]) @ |
128 mat_defs @ pat_defs @ |
115 pat_defs @ |
129 [take_def, finite_def]) |
116 [take_def, finite_def]) |
130 end; (* let (calc_axioms) *) |
117 end; (* let (calc_axioms) *) |
131 |
118 |
132 |
119 |
133 (* legacy type inference *) |
120 (* legacy type inference *) |