Continuity

We define the continuity tactic using aesop.

def attrContinuity : Lean.ParserDescr

The continuity attribute used to tag continuity statements for the continuity tactic.

Equations

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

def tacticContinuity : Lean.ParserDescr

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)

def tacticContinuity? : Lean.ParserDescr

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)