[isabelle-dev] Sort constraints syntax
lp15 at cam.ac.uk
Thu Apr 19 13:22:28 CEST 2012
This sounds like a good idea. The old notation was pretty unreadable.
On 19 Apr 2012, at 12:11, Tobias Nipkow wrote:
> Currently, the sort of a type variable in a type is constrained by attaching
> "::S" to it. Right in the middel of the type, eg "'a::ord => 'a => bool". This
> can make types less readable. In Haskell this is expressed with a separate
> context. After some discussion in Munich we propose to support some such context
> notation, too. The exact syntax is not determined, but something like "[sort
> context] type". The type above could then be written as "['a::ord] 'a => 'a =>
> bool". In this instance it may not even look like an improvement, but with
> larger types and constraints in the middle it does help.
> This would be syntax only and would be translated away with a parse translation.
> It would improve legibility of theory documents. Of course one could also
> imagine types being printed like that.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev