		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Theorem

Fixtype of Syntheto theorems.

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

Fields

name — identifier
variables — typed-variable-list
formula — expression

For now this consists of a name, a list of universally quantified variables, and a formula (a boolean expressions). Unlike ACL2, the universally quantified variables are explicated, with types.

Subtopics

Theorem-fix: Fixing function for theorem structures.
Theorem-equiv: Basic equivalence relation for theorem structures.
Make-theorem: Basic constructor macro for theorem structures.
Theorem->variables: Get the variables field from a theorem.
Theorem->formula: Get the formula field from a theorem.
Change-theorem: Modifying constructor for theorem structures.
Theorem->name: Get the name field from a theorem.
Theoremp: Recognizer for theorem structures.