Email Gateway (Aug 18 2022 at 18:01): Email Gateway (Aug 18 2022 at 18:01):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
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
Email Gateway (Aug 18 2022 at 18:02):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 26 2024 at 12:28 UTC