print type without colon

HOL-Theorem-Prover · Nov 15, 2024 · 633073c · 633073c
1 parent 833b239
commit 633073c
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/src/parse/Parse.sig b/src/parse/Parse.sig
@@ -196,6 +196,7 @@ signature Parse = sig
   val pp_thm : thm pprinter
   val stdprinters : ((term -> string) * (hol_type -> string)) option
 
+  val pp_type_without_colon   : hol_type pprinter
   val term_pp_with_delimiters : term pprinter -> term pprinter
   val type_pp_with_delimiters : hol_type pprinter -> hol_type pprinter
   val get_term_printer : unit -> term pprinter

diff --git a/src/parse/Parse.sml b/src/parse/Parse.sml
@@ -170,6 +170,15 @@ fun update_type_fns () =
 
 val dflt_pinfo = term_pp_utils.dflt_pinfo
 
+fun pp_type_without_colon ty =
+  let
+    open smpp
+    val _ = update_type_fns()
+    val mptr = !type_printer (!current_backend) ty
+  in
+    lower mptr dflt_pinfo |> valOf |> #1
+  end
+
 fun pp_type ty =
   let
     open smpp