|
|
|---|
|
|
|
|---|
Fixtype of premises.
This is a tagged union type, introduced by fty::deftagsum.
We include bindings of the computation state.
Each such binding consists of
a variable for the computation state
(stored in
We also include bindings of single variables that hold (ACL2 models of) C values. (Note that a computation state is not, and does not model, a C value.) These also consist of a variable and a term, like the computation state bindings. However, it is useful to differentiate them in this fixtype, so we can support different processing of the different kind of bindings (as in atc-contextualize).
We also include bindings of multiple variables that hold (ACL2 models of) C values. This is similar to the bindings described in the previous paragraph, but involve mv-let instead of let.
We also include terms that are tests of ifs.
Since the terms used in premises are untranslated, we do not have type constraints on them. In the future, we could use a type for untranslated terms, perhaps a shallow/light recognizer analogous to pseudo-event-formp.
We may add more kinds later.