A helper gadget for annotating nested proofs in goals.
Instances For
Gadget for marking match
-expressions that should not be reduced by the grind
simplifier, but the discriminants should be normalized.
We use it when adding instances of match
-equations to prevent them from being simplified to true.
Instances For
Gadget for representing a = b
in patterns for backward propagation.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.