Continuity #
We define the continuity tactic using aesop.
The continuity attribute used to tag continuity statements for the continuity tactic.
Equations
- attrContinuity = Lean.ParserDescr.node `attrContinuity 1024 (Lean.ParserDescr.nonReservedSymbol "continuity" false)
Instances For
The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the
continuity user attribute.
fun_prop is a (usually more powerful) alternative to continuity.
Equations
- tacticContinuity = Lean.ParserDescr.node `tacticContinuity 1024 (Lean.ParserDescr.nonReservedSymbol "continuity" false)
Instances For
The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the
continuity user attribute.
Equations
- tacticContinuity? = Lean.ParserDescr.node `tacticContinuity? 1024 (Lean.ParserDescr.nonReservedSymbol "continuity?" false)