298 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, |
298 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, |
299 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
299 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
300 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, |
300 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, |
301 ...} : fp_sugar) = |
301 ...} : fp_sugar) = |
302 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
302 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
303 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
303 pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info, |
304 live_nesting_bnfs = live_nesting_bnfs, |
304 fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, |
305 fp_ctr_sugar = |
305 fp_ctr_sugar = |
306 {ctrXs_Tss = ctrXs_Tss, |
306 {ctrXs_Tss = ctrXs_Tss, |
307 ctr_defs = ctr_defs, |
307 ctr_defs = ctr_defs, |
308 ctr_sugar = ctr_sugar, |
308 ctr_sugar = ctr_sugar, |
309 ctr_transfers = ctr_transfers, |
309 ctr_transfers = ctr_transfers, |
324 set_cases = set_cases}, |
324 set_cases = set_cases}, |
325 fp_co_induct_sugar = |
325 fp_co_induct_sugar = |
326 {co_rec = co_rec, |
326 {co_rec = co_rec, |
327 common_co_inducts = common_co_inducts, |
327 common_co_inducts = common_co_inducts, |
328 co_inducts = co_inducts, |
328 co_inducts = co_inducts, |
329 co_rec_def = co_rec_def, |
329 co_rec_def = co_rec_def, |
330 co_rec_thms = co_rec_thms, |
330 co_rec_thms = co_rec_thms, |
331 co_rec_discs = co_rec_disc_thms, |
331 co_rec_discs = co_rec_disc_thms, |
332 co_rec_disc_iffs = co_rec_disc_iffs, |
332 co_rec_disc_iffs = co_rec_disc_iffs, |
333 co_rec_selss = co_rec_sel_thmss, |
333 co_rec_selss = co_rec_sel_thmss, |
334 co_rec_codes = co_rec_codes, |
334 co_rec_codes = co_rec_codes, |