Documentation

Mathlib.Tactic.Continuity

Continuity #

We define the continuity tactic using aesop.

source
def attrContinuity :
Lean.ParserDescr

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

Instances For
    source
    def tacticContinuity :
    Lean.ParserDescr

    The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the continuity user attribute.

    Instances For
      source
      def tacticContinuity? :
      Lean.ParserDescr

      The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the continuity user attribute.

      Instances For