Dimb-table
Fixtype of disambiguation tables.
A disambiguation table associates kinds to identifiers,
with the mapping organized into scopes.
Starting from the outer scope,
i.e. the file scope [C:6.2.1/4],
traversing the code enters and exits
block scopes and prototype scopes [C:6.2.1/4],
in a stack-like fashion.
So we represent a disambiguation table as
a list of disambiguation scopes.
The list should be never empty,
but using :non-emptyp t in this fixtype
generates a false subgoal.
It should be possible to improve fty::deflist
to work with this option in this fixtype,
but for now we just allow empty lists in the fixtype.
Subtopics
- Dimb-tablep
- (dimb-tablep x) recognizes lists where every element satisfies dimb-scopep.
- Dimb-table-fix
- (dimb-table-fix x) is a usual ACL2::fty list fixing function.
- Dimb-table-equiv
- Basic equivalence relation for dimb-table structures.
