Re: [isabelle] print_statement and sorts

On Mon, 30 Jun 2014, Peter Lammich wrote:

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.

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.