*To*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Subject*: Re: [isabelle] Record schemes definition*From*: Makarius <makarius at sketis.net>*Date*: Wed, 6 Jul 2011 10:17:38 +0200 (CEST)*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAL0S8Bew_8gtc9jUxNZXdbCcESoLEtO6u=bebSBwkKwabgydVw@mail.gmail.com>*References*: <CAL0S8Bew_8gtc9jUxNZXdbCcESoLEtO6u=bebSBwkKwabgydVw@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Mon, 4 Jul 2011, Jesus Aransay wrote:

when using Isabelle 2011 and trying to define the following (with nonsense values, but the problem is apparently related to the types, not the values) record: definition v :: "nat ring" where "v = (| carrier = {..(5::nat)}, mult = op +, one = (1::nat), zero = (0::nat), add = op +|)" I do not get any unexpected error. But when I try to "extend" the definition to use record schemes: definition v :: "(nat, 'b) ring_scheme" where "v = (| carrier = {..(5::nat)}, mult = op +, one = (1::nat), zero = (0::nat), add = op +, more=\<dots> |)" I get the following error message: *** exception TERM raised (line 743 of "/usr/local/Isabelle2011/src/HOL/Tools/record.ML"): Error in record input: expecting field Ring.ring.zero but got more *** At command "definition" (line 417 of "/home/jmaransay/Desktop/Jose/Vector_Space_K_n.thy") Is there anything wrong with the second definition?

Makarius

**References**:**[isabelle] Record schemes definition***From:*Jesus Aransay

- Previous by Date: [isabelle] Fwd: 2010 Impact Factor for Journal of Automated Reasoning out now!
- Next by Date: [isabelle] a little problem
- Previous by Thread: [isabelle] Record schemes definition
- Next by Thread: [isabelle] Fwd: 2010 Impact Factor for Journal of Automated Reasoning out now!
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list