Sage Binder (Dec 14 2025 at 04:10): Sage Binder (Dec 14 2025 at 04:10):Hello,
I am trying to print terms with type annotations. I am aware of declare[[show_types]] which seems to add type annotations to variables, but not constants, when printing terms. For instance, suppose the following goal is yielded by running apply (induct xs) on a goal involving an int list.
⋀x y z. 0 < int x ⟹ 0 < int y ⟹ 0 < int z ⟹ set [] ⊆ {int x, int y, int z} ⟹ 0 ≤ sum_list []
In the proof state after the apply, the empty list [] has type int list. However, if I print out this goal with declare[[show_types]] enabled, I get the following.
⋀(x::nat) (y::nat) z::nat.
0 < int x ⟹
0 < int y ⟹ 0 < int z ⟹ set [] ⊆ {int x, int y, int z} ⟹ 0 ≤ sum_list []
The problem is that there are no type annotations on the conclusion 0 ≤ sum_list [], so this cannot be proved (e.g. if I insert this string into a "have" statement verbatim).
Is there any way to print type annotations on everything, including constants?
Dmitriy Traytel (Dec 14 2025 at 11:37):You can get the type information for constants by control-hovering over the constant in question. (This might not work as expected when fancy syntax is used.)
There is also [[show_consts]]. It is not ideal because it prints the type of constants below the goal, so if a constant occurs more than once you'll end up having to guess. But it does help spotting unexpected type variables.
Dmitriy Traytel (Dec 14 2025 at 11:37):(Not sure why this is a question on the Isabelle/ML channel BTW.)
Sage Binder (Dec 14 2025 at 19:19):Sorry, let me clarify a bit.
I am trying to build a tool that takes a goal from an apply-style proof and prints it out in Isar. For instance, if P is a subgoal arising in an apply-style proof, it should become have "P" within some Isar that gets printed to the user. The problem is that without type annotations on constants, some goals become unprovable when printed in Isar (e.g., in my example above, in the term 0 ≤ sum_list [], the type of [] does not match the type of xs).
In ML, I'm using Config.put (Printer.show_types) true to enable the printing of types, and I'm using (Syntax.pretty_term ctxt) |> Pretty.string_of to convert terms to strings. Per your suggestions, I tried using Config.put (show_consts) true as well, but that still does not seem to print types on constants.
Mathias Fleury (Dec 14 2025 at 20:28):What you are describings sounds a lot like Sketch
Mathias Fleury (Dec 14 2025 at 20:30):But explore has the same problem
Mathias Fleury (Dec 14 2025 at 20:30):As a side-remark, I have my own version of explore and never had a problem with types, but that might be due to my goals.
Jonathan Julian Huerta y Munive (Dec 15 2025 at 10:43):@Sage Binder we support several versions of what you want to do in our repository super_sketch_and_super_fix inspired on the Sketch tool Mathias linked above. You can see some examples in the Try_Sketch.thy
Sage Binder (Dec 16 2025 at 18:35):@Jonathan Julian Huerta y Munive Thanks, this looks promising! I'll take a look. Also, the Super Sketch and Super Fix tools look cool :slight_smile:
Sage Binder (Jan 28 2026 at 07:49):@Jonathan Julian Huerta y Munive Thank you for helping me with this question last month! I have been using the following function to print types, which generally works well.
fun print_term ctxt =
singleton (Syntax.uncheck_terms ctxt)
#> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
#> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
#> Sledgehammer_Util.simplify_spaces
However, occasionally I encounter a goal where meta quantifiers get printed as Pure.all instead of the usual syntax. This seems sporadic and I really have no idea what causes it. For example, the goal
⋀x y. i ≤ n ⟹
j ≤ n ⟹
i ≠ j ⟹
transpos i j y ≤ n ⟹
y ≤ n ⟹
transpos i j y ≠ i ⟹ transpos i j y ≠ j ⟹ y ≠ i ⟹ y ≠ j ⟹ transpos i j y = y
gets printed as
Pure.all ((λx::nat. (⋀y::nat. ⟦(i::nat) ≤ (n::nat); (j::nat) ≤ n; i ≠ j; transpos i j y ≤ n; y ≤ n; transpos i j y ≠ i; transpos i j y ≠ j; y ≠ i; y ≠ j⟧ ⟹ transpos i j y = y))::nat ⇒ prop)
(This is a random goal from Algebra1.thy in the Group-Ring-Module AFP entry; I wish I could find a shorter example but like I said, the problem is seemingly random). Notably, this term with Pure.all does not type check, with the error: Operator: Trueprop :: bool ⇒ prop. Manually changing the Pure.all to the usual ⋀ syntax fixes the type issue.
I wonder if you have ever encountered this with Super Sketch, or if you have any idea how to solve this. Perhaps a custom version of the Sledgehammer_Isar_Annotate.annotate_types_in_term function is necessary?
Kevin Kappelmann (Jan 28 2026 at 09:29):I think annotate_types introduced a _type_constraint_ constant in your example. You can strip these constraints with Type.strip_constraints. Maybe the following modification to your code works for your applications?
fun print_term ctxt =
singleton (Syntax.uncheck_terms ctxt)
#> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
#> Type.strip_constraints (*new line*)
#> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
#> Sledgehammer_Util.simplify_spaces
@Sage Binder I tried your goal with the Sketcher functions and everything worked as expected on our side. I also tried Kevin's suggestion and that seems to do the fix for your goal:
ML ‹
fun print_term ctxt =
singleton (Syntax.uncheck_terms ctxt)
#> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
#> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
#> Sledgehammer_Util.simplify_spaces;
fun print_term' ctxt =
singleton (Syntax.uncheck_terms ctxt)
#> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
#> Type.strip_constraints (*new line*)
#> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
#> Sledgehammer_Util.simplify_spaces;
›
lemma "⋀x y. i ≤ n ⟹
j ≤ n ⟹
i ≠ j ⟹
transpos i j y ≤ n ⟹
y ≤ n ⟹
transpos i j y ≠ i ⟹ transpos i j y ≠ j ⟹ y ≠ i ⟹ y ≠ j ⟹ transpos i j y = y"
ML_val ‹
val t1 = print_term \<^context> (Thm.prop_of (#goal (Proof.goal (Toplevel.proof_of @{Isar.state}))));
val t1 = print_term' \<^context> (Thm.prop_of (#goal (Proof.goal (Toplevel.proof_of @{Isar.state}))));
val _ = Sketcher.sketch_goals_at Sketcher.FIX_SHOW 2 @{Isar.state}
|> Sketcher.make_skeleton 0 "-"
|> Output.information o Active.sendback_markup_command
›
It appears that Kevin's solution does prevent the Pure.all issue, but it also removes type annotations on constants, which runs into the initial issue I described in this thread. It seems the Sketcher.make_skeleton actually has the same issue. Going back to the original example I presented:
lemma "⋀x y z.
0 < int x
⟹ 0 < int y
⟹ 0 < int z
⟹ set [] ⊆ {int x, int y, int z}
⟹ (0::int) ≤ sum_list []"
ML_val ‹
val t1 = print_term \<^context> (Thm.prop_of (#goal (Proof.goal (Toplevel.proof_of @{Isar.state}))));
val t2 = print_term' \<^context> (Thm.prop_of (#goal (Proof.goal (Toplevel.proof_of @{Isar.state}))));
val _ = Sketcher.sketch_goals_at Sketcher.FIX_SHOW 2 @{Isar.state}
|> Sketcher.make_skeleton 0 "-"
|> Output.information o Active.sendback_markup_command
›
proof-
fix x :: "nat"
and y :: "nat"
and z :: "nat"
assume "0 < int x"
and "0 < int y"
and "0 < int z"
and "set [] ⊆ {int x, int y, int z}"
thus goal0: "0 ≤ sum_list []" (* 0 :: 'a, but should be int*)
sorry
qed
The goal0 will not be provable because 0 needs to be annotated to be an int.
It seems that the type constraints which enable type annotations on constants (what I want) also causes the meta quantifier to (sometimes) be printed as Pure.all (what I don't want).
Sage Binder (Jan 28 2026 at 20:33):I'm wondering if I can modify the strip_constraints function to only affect the particular constraint that is causing the Pure.all issue. I guess it is something involving prop?
Sage Binder (Jan 28 2026 at 20:54):Ok, I've modified strip_constraints to only strip constraints that contain "prop". I guess this is a bit hacky, but I think it will work for my purposes.
fun
strip_prop_constraints ctxt ((c as Const ("_type_constraint_", ty)) $ t) =
if String.isSubstring "prop" (Syntax.string_of_typ ctxt ty) then
strip_prop_constraints ctxt t
else
c $ strip_prop_constraints ctxt t
| strip_prop_constraints ctxt (t $ u) = strip_prop_constraints ctxt t $ strip_prop_constraints ctxt u
| strip_prop_constraints ctxt (Abs (x, T, t)) = Abs (x, T, strip_prop_constraints ctxt t)
| strip_prop_constraints _ a = a;
I suspect that there will be similar issues (e.g. with other binders that don't live in prop) that you will miss (e.g. HOL.All).
But pushing that aside, here's a more elegant way to check if a type contains prop:
ML‹
val contains_prop = exists_subtype (can \<^Type_fn>‹prop => ‹()››)
val _ = @{print} (contains_prop @{typ "bool ⇒ (prop ⇒ bool)"})
val _ = @{print} (contains_prop @{typ "bool ⇒ (bool ⇒ bool)"})
›
After further testing, I did indeed encounter similar issues with HOL.All (though it seems much rarer, for some reason). Luckily, for my purposes this is fine, since have "All (λx. [...])" does not result in a type error like it does with Pure.all.
Thank you all for the help!
Lukas Bartl (Jan 30 2026 at 12:09):The issue with Pure.all seems to be a problem with Sledgehammer_Isar_Annotate.annotate_types_in_term. I will try to look into it, when I have time. It seems to happen if x (the first variable) is not used. Here is a minimal example (gets printed as Pure.all ((λx. (⋀y. y = y))::'a ⇒ prop)):
ML‹@{term "⋀x y. y = y"}
|> singleton (Syntax.uncheck_terms @{context})
|> Sledgehammer_Isar_Annotate.annotate_types_in_term @{context}
|> Syntax.unparse_term (Config.put show_markup false (Config.put show_types false @{context}))›
In your print_term function, Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) should nowadays be replaced by Syntax.unparse_term ctxt #> Pretty.pure_string_of (as done in Sketch and Sledgehammer_Isar_Proof).
Concerning your original problem annotating constants with types: Sledgehammer_Isar_Annotate introduces type annotations where necessary, but you have to configure the printer accordingly, such that these are displayed: Sketch and Sledgehammer_Isar_Proof use [[show_markup=false, show_types=false]], which works for variables, but does not display type annotations on constants. Here is a minimal example, which is displayed as 0 instead of 0::nat:
ML‹@{term "0::nat"}
|> singleton (Syntax.uncheck_terms @{context})
|> Sledgehammer_Isar_Annotate.annotate_types_in_term @{context}
|> Syntax.unparse_term (Config.put show_markup false (Config.put show_types false @{context}))›
If you replace 0 by x, it is displayed as x::nat. If you use true instead of false (i.e., using [[show_types]]), 0 is displayed as 0::nat, but x is displayed as (x::nat)::nat which works but has an unnecessary second annotation.
Last updated: Feb 04 2026 at 02:22 UTC