		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Fact-infop

Recognize information about facts.

(fact-infop x) is a std::defaggregate of the following fields.

thm-name — Invariant (symbolp thm-name).
formula — An untranslated term.

Source link: fact-infop

Facts are stored in an alist from their names to this information, which consists of the name of the theorem generated for the fact and the formula of the theorem (i.e. the fact).

Subtopics

Make-fact-info: Constructor macro for fact-infop structures.
Fact-info: Raw constructor for fact-infop structures.
Change-fact-info: A copying macro that lets you create new fact-infop structures, based on existing structures.
Make-honsed-fact-info: Constructor macro for honsed fact-infop structures.
Honsed-fact-info: Raw constructor for honsed fact-infop structures.
Fact-info->thm-name: Access the thm-name field of a fact-infop structure.
Fact-info->formula: Access the formula field of a fact-infop structure.