Bed-mk1
Low-level functions for constructing BEDs.
- Signature
(bed-mk1) → *
Definitions and Theorems
Function: bed-mk1
(defun bed-mk1 nil
(declare (xargs :guard t))
(let ((__function__ 'bed-mk1))
(declare (ignorable __function__))
nil))
Subtopics
- Mk-op-reorder
- Construct a reduced BED using bed-order.
- Bed-order
- Ordering mechanism for canonicalizing symmetric operators.
- Mk-not
- Construct a reduced BED for not(x).
- Mk-op1
- Operator node constructor with basic reductions.
- Mk-op-x-x
- Construct a reduced BED for op(arg, arg).
- Mk-op-x-true
- Construct a reduced BED for op(left, true).
- Mk-op-x-false
- Construct a reduced BED for op(left, false).
- Mk-op-true-x
- Construct a reduced BED for op(true, right).
- Mk-op-false-x
- Construct a reduced BED for op(false, right).
- Bed-match-var
- Pattern match a variable ITE node.
- Mk-var1
- Variable node constructor with basic reductions.
- Mk-const-prop
- Mk-op-raw
- Raw construct for an binary operator node.
- Mk-var-raw
- Raw constructor for a variable ITE node.
