Universal Quantifiers
The forall function expresses that a property holds for all values of a type. It is a verification construct: use it in contracts, ghost code, invariants, assertions, and lemmas, not as runtime control flow.
Existential Quantifiers
The exists function expresses that at least one value of a type satisfies a property. It is a verification construct for contracts, ghost code, assertions, invariants, and lemmas, not a runtime search operation.
Triggers
Triggers guide the SMT solver when instantiating quantified formulas. Use forallWith to provide explicit triggers when automatic inference is insufficient or causes performance issues.
Quantifier Patterns
Common quantifier idioms for real-world verification scenarios.