Re: [isabelle] Record schemes definition



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?

The syntax for the "more" pseudo field is "..." or "\<dots>". Moreover, the \<dots> value above actually refers to the builtin term abbreviation of Isar calculations (which is unbound in the avove situation).

I can't say on the spot why the error message from the record package is not more precise -- it has a bit too many features accumulated over the years.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.