On Fri, 6 Jul 2012, Tobias Nipkow wrote:
You write
The notation would have to prevent any misinterpretation as a local
context or binder just for the type in question.
But that is what is intended. If you look at the prototype that I had
sent you separately, you see that ['a::S]T is just
On Thu, 19 Apr 2012, 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
You write
The notation would have to prevent any misinterpretation as a local context or
binder just for the type in question.
But that is what is intended. If you look at the prototype that I had sent you
separately, you see that ['a::S]T is just replaced by T['a::S/'a] upon
parsing. A good old
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
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
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
Reactions?
Postpone discussion until after official rollout of Isabelle2012.
There still many things to be sorted out.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
I did not propose to add this before the release, but I don't see any harm in
discussing it now. In fact, now people may be more alert than later. Of course
you are welcome to add your two cents later.
Tobias
Am 19/04/2012 13:25, schrieb Makarius:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
I did not propose to add this before the release, but I don't see any
harm in discussing it now. In fact, now people may be more alert than
later. Of course you are welcome to add your two cents later.
I do see a harm. A release is not a trivial
As I said: add them later.
Tobias
Am 19/04/2012 14:09, schrieb Makarius:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
I did not propose to add this before the release, but I don't see any harm in
discussing it now. In fact, now people may be more alert than later. Of
course
you are welcome
