Re: [isabelle] print_statement and sorts
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] print_statement and sorts
- From: Makarius <makarius at sketis.net>
- Date: Fri, 25 Jul 2014 16:31:31 +0200 (CEST)
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <1404122749.20661.113.camel@lapbroy33>
- References: <1404122749.20661.113.camel@lapbroy33>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and