equal
deleted
inserted
replaced
121 val sel_defs = let |
121 val sel_defs = let |
122 fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == |
122 fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == |
123 list_ccomb(%%:(dname^"_when"),map |
123 list_ccomb(%%:(dname^"_when"),map |
124 (fn (con',args) => if con'<>con then UU else |
124 (fn (con',args) => if con'<>con then UU else |
125 List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); |
125 List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); |
126 in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; |
126 in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end; |
127 |
127 |
128 |
128 |
129 (* ----- axiom and definitions concerning induction ------------------------- *) |
129 (* ----- axiom and definitions concerning induction ------------------------- *) |
130 |
130 |
131 val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n |
131 val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n |