Email Gateway (Aug 19 2022 at 14:39): Email Gateway (Aug 19 2022 at 14:39):From: Peter Lammich <lammich@in.tum.de>
Hi all,
print_statement is a nice feature, as it prints a theorem in long-goal
format, ready to be copied into the edit-buffer, e.g. to slightly modify
it.
However, if sorts are involved, the printed statement is, in many cases,
just not valid, as sort constraints are omitted:
print_statement order_refl
theorem order_refl:
fixes x :: "'a"
shows "x ≤ x"
*** Type unification failed: Variable 'a::type not of sort ord
Using show_sorts is also not what I really want, as the sort-annotations
pop up in the term, too:
theorem order_refl:
fixes x :: "'a∷preorder"
shows "(x∷'a∷preorder) ≤ x"
The best way might be to make print_statement only print non-default
sorts in the fixes-part.
Email Gateway (Aug 19 2022 at 15:04):From: Makarius <makarius@sketis.net>
There is a deeper problem here: the simulteneous "uncheck" phase for
types/terms before printing should take care of constraints, and reduce
them to a sensible minimum. It doesn't do that for various historic
reasons: the scope is just a single type or term.
It has required some years to make the dual "check" phase use constraints
simulteneously, and "uncheck" might require some time to get there as
well.
Makarius
Last updated: Apr 24 2024 at 20:16 UTC