		Search-engine friendly clone of the ACL2 documentation.

Files

Var/const-sort

Fixtype of sorts of variables and constants.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:public → var/const-sort-public
:private → var/const-sort-private
:constant → var/const-sort-constant
:const → var/const-sort-const

There are currently four sorts (i.e. kinds) of variables and constants: public variables, private variables, constant-designated constants, and const-designated constants. It is likely that the latter two will be unified, but for now we follow the grammar and have two.

These variable and constant sorts are used for function parameters and for input file items.

Subtopics

Var/const-sort-fix: Fixing function for var/const-sort structures.
Var/const-sort-case: Case macro for the different kinds of var/const-sort structures.
Var/const-sort-equiv: Basic equivalence relation for var/const-sort structures.
Var/const-sortp: Recognizer for var/const-sort structures.
Var/const-sort-kind: Get the kind (tag) of a var/const-sort structure.
Var/const-sort-public
Var/const-sort-private
Var/const-sort-constant
Var/const-sort-const