Macros§
- decreases_
to - decreases_to!(b => a) means that height(a) < height(b), so that b can decrease to a in decreases clauses. decreases_to!(b1, …, bn => a1, …, am) can compare lexicographically ordered values, which can be useful when making assertions about decreases clauses. Notes:
- decreases_
to_ internal - with_
triggers
Structs§
- FnProof
- FnProof is the type of proof closures; the syntax proof_fn is used to wrap FnProof
- FnSpec
- Ghost
- NoCopy
- Proof
FnConfirm - Spec
Chain - Tracked
- int
- nat
- real
Constants§
Traits§
- Boolean
- Chainable
- Decimal
- Ieee
Float - Ieee
Float Cast - Integer
- ProofFn
- Proof
FnMut - Proof
FnOnce - Proof
FnReq Ens - Proof
FnReq EnsDef - SpecAdd
- Spec
BitAnd - Spec
BitOr - Spec
BitXor - SpecEq
- Spec
Euclidean Mod - Spec
Euclidean OrReal Div - SpecMul
- SpecNeg
- SpecOrd
- SpecShl
- SpecShr
- SpecSub
- Structural
- derive(Structural) means that exec-mode == and ghost == always yield the same result. derive(Structural) is only allowed when all the fields of a type are also Structural. derive(StructuralEq) means derive(Structural) and also implement PartialEqSpec, setting eq_spec to == and obeys_eq_spec to true.