		Search-engine friendly clone of the ACL2 documentation.

Verified

Verified part of Smtlink

Uninterpreted-fn-cp: Verified clause-processor for proving return types of uninterpreted functions.
Smt-hint-interface: Define default Smtlink hint interface
Function-expansion: Function expansion
Smt-config: Define default Smtlink config and custom Smtlink config
Fty-support: Supports for ftytypes
Smt-computed-hints: This document discusses how computed-hints are used in the architecture of Smtlink.
Add-hypo-cp: Verified clause-processor for adding user hypotheses
Smt-hint-please: The function hint-please in SMT is for passing hints to subgoals using the clause-processor and computed-hint mechanism.
Type-extract-cp: Verified clause-processor for extracting type declarations
Smt-extract: SMT-extract extracts type hypotheses from the clause. The SMT solver requires knowing type declarations.
Smtlink-process-user-hint: Functionalities for processing user hints given to Smtlink. User hints will be merged with (smt-hint).
Smt-basics: Basic functions and types in Smtlink.
Smt-type-hyp: The function type-hyp passes type related information onto the trusted clause processor.
Smt-magic-fix