Re-exports§
pub use prop::Prop;
Modules§
Structs§
- Axiom
- Builder
- Case
Name - Checked
Sig - FunOp
- Gen
- A bit of state used to auto-generate fresh variable names.
- Goal
- Hypothetical
Call - Hypothetical
Call Syntax - Inst
Rule - Inst
Rule Syntax - Match
Arm - OpCode
- PredOp
- Pred
Symbol - RecOp
- RirFn
- RirFn
Sig - Sig
- Type
Context
Enums§
- BType
- A BType is a base type, which can be represented directly by a sort.
- Binder1
- Computations that bind a single variable for use in a body computation.
- BinderN
- Computations that bind multiple variables for use in a body computation.
- CType
- Comp
- Inst
Mode - Literal
- LogOpN
- A logical operator that takes zero or more arguments.
- Oc
- Op
- OpMode
- Pattern
- Quantifier
- Rebuild
- TypeDef
- VName
- Variable names
- VType
- A VType is a base type or a tuple
- Val