[isabelle] Record field names and accessing other constants



Hi people,

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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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