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:
Last updated: Dec 17 2025 at 08:33 UTC