[isabelle-dev] Sort constraints syntax

[Lawrence Paulson]

This sounds like a good idea. The old notation was pretty unreadable.
Larry

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.
> 
> Reactions?
> 
> Tobias
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev