[isabelle] Record schemes definition



Dear all,

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?

Thanks in advance for any hint,

Jesus

-- 
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España





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