Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- Decidable
Counter - A counter that tracks how many decisions have been made and their outcomes.
- Decidable
Prop Ext - Extended decidable proposition structure.
- Decidable
SetExt - Decidable membership for a finite set.
- Decision
Chain - A sequential chain of decisions where each step can depend on the previous.
- Decision
Procedure Ext - Decision procedure (DPLL, tableaux, resolution, etc.).
- Decision
Table - A lookup table of named decidable propositions.
- EqDecision
- A decidable equality check wrapper.
- Finite
Set - A finite set with decidable membership.
- FnPred
- A function-based decidable predicate.
- Halting
Oracle Ext - Halting oracle (exists only non-constructively, for axiom purposes).
- Interval
- A closed integer interval
[lo, hi]. - LeDecision
- A decidable ordering check wrapper.
- Named
Decision - A decision tagged with a human-readable name for debugging.
- Not
- A negation proof: evidence that
Pdoes not hold. - Semi
Decidable Ext - Semi-decidable (recursively enumerable) predicate.
Enums§
- Bool
Reflect - Reflection between
booland decidable propositions. - Decision
- A decision about a proposition
P.