		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation

Soft-implementation-core

Core implementation code of SOFT.

Subtopics

Sothm-inst-facts: Create list of facts for functional instantiation.
Ext-fun-subst-term/terms/function: Extend function substitutions for functional instantiation.
Fun-subst-function: Apply a function substitution to an individual function.
Sothm-inst-pairs: Create a list of doublets for functional instantiation.
Funvars-of-term/terms: Function variables that terms depend on.
Funvars-of-plain-fn: Function variables depended on by a plain second-order function or by an instance of it.
Sothm-inst-proof: Proof builder instructions to prove instances of second-order theorems.
Fun-subst-term/terms: Apply function substitutions to terms.
Get-sof-instance: Retrieve the instance associated to a given instantiation, in the map of known instances of a second-order function.
Sof-instancesp: Recognize the information about the instances that is associated to second-order function names in the sof-instances table.
Put-sof-instance: Associates an instantiation with an instance in an existing map of know instances of a second-order function.
Fun-substp: Recognize function substitutions.
Sofun-kindp: Recognize symbols that denote the kinds of second-order functions supported by SOFT.
Funvar-listp: Recoegnize true lists of function variables.
*-listp: Recognize true lists of *s.
Funvars-of-quantifier-fn: Function variables depended on by a quantifier second-order function or by an instance of it.
No-trivial-pairsp: Check if an alist has no pairs with equal key and value.
Funvars-of-choice-fn: Function variables depended on by a choice second-order function or by an instance of it.
Funvar-instp: Recognize instantiations.
Funvars-of-thm: Function variables depended on by a second-order theorem or by an instance of it.
Sofunp: Recognize names of second-order functions.
Funvarp: Recognize names of function variables.
Sof-instances: Known instances of a second-order function.
Sothmp: Recognize second-order theorems.
Quant-sofunp: Recognize quantifier second-order functions.
Plain-sofunp: Recognize plain second-order functions.
Funvar-inst-listp: Recognize true lists of instantiations.
Choice-sofunp: Recognize choice second-order functions.
Sofun-funvars: Function variables that a second-order function depends on.
Sofun-kind: Kind of a second-order function.
Function-variables-table: Table of function variables.
Sof-instances-table: Table of instances of second-order functions.
Second-order-functions-table: Table of second-order functions.