		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Expr-sort

Fixtype of expression sorts.

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

Member Tags → Types

:constant → expr-sort-constant
:nonconst → expr-sort-nonconst
:location → expr-sort-location

There are three sorts of expressions: those that evaluate to a constant value; those that evaluate to a non-constant value; and those that evaluation to a location. These three possibilities are captured here.

Subtopics

Expr-sort-case: Case macro for the different kinds of expr-sort structures.
Expr-sort-fix: Fixing function for expr-sort structures.
Expr-sort-equiv: Basic equivalence relation for expr-sort structures.
Expr-sortp: Recognizer for expr-sort structures.
Expr-sort-nonconst
Expr-sort-location
Expr-sort-kind: Get the kind (tag) of a expr-sort structure.
Expr-sort-constant