Hi Bertram,
just a curious question: in which context are you using the Isabelle
code generator?
CU,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
__
Hi Bertram,
> the Haskell code generator of Isabelle currently emits contexts for
> data and newtype generates, e.g. (from CeTA):
>
> newtype (Linorder a) => Rbt a b = Rbt (Rbta a b);
>
> The sole effect of such contexts is that the programmer must provide
> a (Linorder a) context wherever Rbt
Hi all,
recently I thought about something which is slightly related to giving
sort constraints for datatypes (but also raised a completely unrelated
question). Let me just give my idea:
Currently I am working on a formalization of Kruskal's Tree Theorem (but
I am still far from finished ;))
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
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
Dear Isabelle developers,
the Haskell code generator of Isabelle currently emits contexts for
data and newtype generates, e.g. (from CeTA):
newtype (Linorder a) => Rbt a b = Rbt (Rbta a b);
The sole effect of such contexts is that the programmer must provide
a (Linorder a) context wherever Rbt
16 matches
Mail list logo