718 SOME {Rep_name, ...} => s = Rep_name |
718 SOME {Rep_name, ...} => s = Rep_name |
719 | NONE => false) |
719 | NONE => false) |
720 | is_rep_fun _ _ = false |
720 | is_rep_fun _ _ = false |
721 fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, |
721 fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, |
722 [_, abs_T as Type (s', _)]))) = |
722 [_, abs_T as Type (s', _)]))) = |
723 try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' |
723 try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s' |
724 = SOME (Const x) andalso not (is_codatatype ctxt abs_T) |
724 = SOME (Const x) andalso not (is_codatatype ctxt abs_T) |
725 | is_quot_abs_fun _ _ = false |
725 | is_quot_abs_fun _ _ = false |
726 fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, |
726 fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, |
727 [abs_T as Type (s', _), _]))) = |
727 [abs_T as Type (s', _), _]))) = |
728 try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' |
728 try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s' |
729 = SOME (Const x) andalso not (is_codatatype ctxt abs_T) |
729 = SOME (Const x) andalso not (is_codatatype ctxt abs_T) |
730 | is_quot_rep_fun _ _ = false |
730 | is_quot_rep_fun _ _ = false |
731 |
731 |
732 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun}, |
732 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun}, |
733 [T1 as Type (s', _), T2]))) = |
733 [T1 as Type (s', _), T2]))) = |