source
def Lean.Order.monotonicity :
ParserDescr

`monotonicity` performs one compositional step solving `monotone` goals, using lemma tagged with `@[partial_fixpoint_monotone]`.

This tactic is mostly used internally by lean in `partial_fixpoint` definitions, but can be useful on its own for debugging or when proving new `@[partial_fixpoint_monotone]` lemmas.

Equations

- Lean.Order.monotonicity = Lean.ParserDescr.node `Lean.Order.monotonicity 1024 (Lean.ParserDescr.nonReservedSymbol "monotonicity" false)

Instances For