[isabelle] print_statement and sorts
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
However, if sorts are involved, the printed statement is, in many cases,
just not valid, as sort constraints are omitted:
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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and