This is an interesting issue. I would like to know if we need class constraints
for datatype parameters in the first place. I thought we had agreed at some
point (not on this list) to get rid of them, but we never did. Maybe there are
situations where you need them? The only one that comes to my
On Tue, 8 May 2012, Tobias Nipkow wrote:
This is an interesting issue. I would like to know if we need class
constraints for datatype parameters in the first place. I thought we had
agreed at some point (not on this list) to get rid of them, but we never
did. Maybe there are situations where
Am 08/05/2012 12:01, schrieb Makarius:
On Tue, 8 May 2012, Tobias Nipkow wrote:
This is an interesting issue. I would like to know if we need class
constraints for datatype parameters in the first place. I thought we had
agreed at some point (not on this list) to get rid of them, but we
On Tue, 8 May 2012, Tobias Nipkow wrote:
I mean the datatype definition facility.
Over the years this lead to occasional confusion of end-users, who
wanted to restrict their datatype constructors on purpose. (I can dig
up an email by Elsa Gunter from the late 1990-ies, if you want.)
It is
On Wed, 2 May 2012, Brian Huffman wrote:
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
is it really the case that currently the only way to obtain ASCII output
using print modes is by specifying the empty string, like
thm () conjE
or did I miss anything?
On Wed, 2 May 2012, Christian Sternagel wrote:
would it make sense to introduce some kind of read-only mode for
theory files and then use this mode when jumping to a file that is
already finished (instead of the Attempt to update loaded theory ...
error message)?
Of course I don't know
On Di, 2012-05-08 at 12:55 +0200, Tobias Nipkow wrote:
Am 08/05/2012 12:41, schrieb Makarius:
On Tue, 8 May 2012, Tobias Nipkow wrote:
I mean the datatype definition facility.
Over the years this lead to occasional confusion of end-users, who wanted
to
restrict their datatype
On Tue, 8 May 2012, Tobias Nipkow wrote:
I mean the datatype definition facility.
Over the years this lead to occasional confusion of end-users, who
wanted to restrict their datatype constructors on purpose. (I can
dig up an email by Elsa Gunter from the late 1990-ies, if you want.)
Kudos
Am 08/05/2012 13:49, schrieb Peter Lammich:
datatype a'::heap linked_list = nil | node 'a 'a linked_list ref
Actually, I think this does not do what you hope it does, hence the magic is
still in there. But Lukas showed me a related defn:
datatype 'a ref = Ref nat
where 'a is a phantom type but
Am 08/05/2012 14:44, schrieb Makarius:
So apart from the observation that the foundational kernel does not require
sort
constraints (apart from HOL.type of course), were there any reasons against
them?
They are not allowed in Haskell anymore, so why do we allow them (and complicate
the code
On Tue, 8 May 2012, Makarius wrote:
I did not find these ancient mails in my folders from the mid-1990-ies on the
spot.
At last, I've found my mail folders before the year 1996. On 29-Sep-1994
someone was pointing out that latest Gofer and Haskell would now support
type class constraints
On Tue, 8 May 2012, Tobias Nipkow wrote:
Am 08/05/2012 14:44, schrieb Makarius:
So apart from the observation that the foundational kernel does not require sort
constraints (apart from HOL.type of course), were there any reasons against
them?
They are not allowed in Haskell anymore, so why
12 matches
Mail list logo
