		Search-engine friendly clone of the ACL2 documentation.

Statements

Constdecl

Fixtype of constant declarations.

This is a product type introduced by fty::defprod.

Fields

name — identifier
type — type
init — expression

A constant declaration has the same structure as a variable declaration, but we introduce a different type because variables and constants are different entities and also so that it is easier to extend variable or constant declarations independently from each other, should the need arise.

Subtopics

Constdecl-fix: Fixing function for constdecl structures.
Constdecl-equiv: Basic equivalence relation for constdecl structures.
Make-constdecl: Basic constructor macro for constdecl structures.
Constdeclp: Recognizer for constdecl structures.
Change-constdecl: Modifying constructor for constdecl structures.
Constdecl->type: Get the type field from a constdecl.
Constdecl->name: Get the name field from a constdecl.
Constdecl->init: Get the init field from a constdecl.