Soft-macros
Macros provided by SOFT.
defunvar,
defsoft,
defun2,
defund2,
defchoose2,
defun-sk2,
define2, and
define-sk2
are wrappers of existing events
that record function variables and dependencies of functions on them.
They set the stage for defun-inst and defthm-inst.
defun-inst provides the ability to concisely generate functions,
and automatically prove their termination if recursive,
by specifying replacements of function variables.
defthm-inst provides the ability to
concisely generate and automatically prove theorems,
by specifying replacements of function variables.
Subtopics
- Defun-inst
- Introduce a function by instantiating a second-order functions.
- Defequal
- Introduce an equality between functions.
- Defsoft
- Record an existing function as second-order.
- Defthm-inst
- Introduce a theorem by instantiating a second-order theorem.
- Defun2
- Introduce a second-order function
via a second-order version of defun.
- Defunvar
- Introduce a function variable.
- Defun-sk2
- Introduce a second-order function
via a second-order version of defun-sk.
- Defchoose2
- Introduce a second-order function
via a second-order version of defchoose.
- Defthm-2nd-order
- Introduce a second-order theorem.
- Define-sk2
- Introduce a second-order function
via a second-order version of std::define-sk.
- Defund-sk2
- Introduce a second-order function
via a second-order version of ACL2::defund-sk.
- Define2
- Introduce a second-order function
via a second-order version of define.
- Defund2
- Introduce a second-order function
via a second-order version of defund.
