Email Gateway (Aug 19 2022 at 10:03): Email Gateway (Aug 19 2022 at 10:03):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Email Gateway (Aug 19 2022 at 10:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Yannick,
You can refer to all constants with their unique long name (unless
access has been disabled explicitly with hide_const). In your example,
you can refer to y introduced in the consts declaration as TheoryName.y
where TheoryName is the name of the theory that contains the
declaration. Side remark: Name hiding is not specific to the record package.
Best,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC