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
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 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
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
12 matches
Mail list logo
