src/HOL/Tools/Nunchaku/nunchaku_problem.ML
 changeset 66622 0916eb2dbaca parent 66618 048524a4f537 child 66623 8fc868e9e1bf
equal inserted replaced
66621:1eb8e87f7f8b 66622:0916eb2dbaca
712
712
713 fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =
713 fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =
714   str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
714   str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
715   (case subset of
715   (case subset of
716     NONE => ""
716     NONE => ""
717   | SOME s => if is_triv_subset s then "" else "\n  " ^ nun_subset ^ " " ^ str_of_tm s) ^
717   | SOME s =>

718     if is_triv_subset s then ""

719     else "\n  " ^ nun_subset ^ " " ^ nun_parens_if_space (str_of_tm s)) ^
718   (* TODO: use nun_quotient when possible *)
720   (* TODO: use nun_quotient when possible *)
719   (case quotient of
721   (case quotient of
720     NONE => ""
722     NONE => ""
721   | SOME q => "\n  " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^
723   | SOME q => "\n  " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^
722   "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;
724   "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;