Continuity

We define the continuity tactic using aesop.

def attrContinuity : Lean.ParserDescr

@[continuity] adds the tagged definition to the set of lemmas used by the continuity tactic. Lemmas are used without backtracking: when the conclusion of this lemma matches the goal, the lemma is applied unconditionally. Thus a lemma should preserve provability: if the goal can be proven, then after applying a @[continuity] lemma to it, the generated subgoals should remain provable.

Equations

• attrContinuity = Lean.ParserDescr.node `attrContinuity 1024 (Lean.ParserDescr.nonReservedSymbol "continuity" false)

def tacticContinuity : Lean.ParserDescr

continuity solves goals of the form Continuous f by applying lemmas tagged with the attribute @[continuity]. If the goal is not solved after attempting all rules, continuity fails.

fun_prop is a (usually more powerful) alternative to continuity.

This tactic is extensible. Tagging lemmas with the @[continuity] attribute can allow continuity to solve more goals.

• continuity? reports the proof script found by continuity.

Equations

• tacticContinuity = Lean.ParserDescr.node `tacticContinuity 1024 (Lean.ParserDescr.nonReservedSymbol "continuity" false)

def tacticContinuity? : Lean.ParserDescr

continuity solves goals of the form Continuous f by applying lemmas tagged with the attribute @[continuity]. If the goal is not solved after attempting all rules, continuity fails.

fun_prop is a (usually more powerful) alternative to continuity.

This tactic is extensible. Tagging lemmas with the @[continuity] attribute can allow continuity to solve more goals.

• continuity? reports the proof script found by continuity.

Equations

• tacticContinuity? = Lean.ParserDescr.node `tacticContinuity? 1024 (Lean.ParserDescr.nonReservedSymbol "continuity?" false)