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 d
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
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 c
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 b
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
On 05/08/2012 01:49 PM, Peter Lammich wrote:
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 wan
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
> >>> restri
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 w
On Wed, 2 May 2012, Brian Huffman wrote:
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
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? Since this print mode
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 constructors on purpose. (I can dig up an email by
>>> El
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
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
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 y
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 mi
14 matches
Mail list logo
