[isabelle] Record field names and accessing other constants
A record field defines a constant of type function, which is the accessors
of the field. There's a way to disambiguate between multiple of such
constants, selecting the one of a same name of different records, using a
prefix; but I don't see or don't know a way to select one of a same name
of the whole theory scope.
A sample case:
consts y :: bool
consts z :: bool
record u = x :: bool
record v = x :: bool y :: bool
term "(| u.x = y |)"
term "(| v.x = y, v.y = y |)"
Both above terms has are erroneous, due to type error with “y”,
interpreted as “v.y” (substituting “= y” to “= z” is OK). I can select “x”
from “u” or “v” using the corresponding prefixes, but I don't know how to
select the “y” defined prior to the records definitions.
Is there a prefix to select the “y::bool” constant?
The case occurred during investigation, not during a real case, so that's
not blocking for now, but it teases me enough to make me open this thread.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and