equal
deleted
inserted
replaced
147 (thm', ctxt') |
147 (thm', ctxt') |
148 end |
148 end |
149 |
149 |
150 fun equivariance pred_trms raw_induct intrs ctxt = |
150 fun equivariance pred_trms raw_induct intrs ctxt = |
151 let |
151 let |
|
152 val is_already_eqvt = |
|
153 filter (is_eqvt ctxt) pred_trms |
|
154 |> map (Syntax.string_of_term ctxt) |
|
155 val _ = if null is_already_eqvt then () |
|
156 else error ("Already equivariant: " ^ commas is_already_eqvt) |
|
157 |
152 val pred_names = map (fst o dest_Const) pred_trms |
158 val pred_names = map (fst o dest_Const) pred_trms |
153 val raw_induct' = atomize_induct ctxt raw_induct |
159 val raw_induct' = atomize_induct ctxt raw_induct |
154 val intrs' = map atomize_intr intrs |
160 val intrs' = map atomize_intr intrs |
155 val (([raw_concl], [raw_pi]), ctxt') = |
161 val (([raw_concl], [raw_pi]), ctxt') = |
156 ctxt |
162 ctxt |