Documentation

Lean.Meta.Tactic.Congr

source
def Lean.MVarId.congrPre (mvarId : Lean.MVarId) :
Lean.MetaM (Option Lean.MVarId)

Preprocessor before applying congruence theorem. Tries to close new goals using Eq.refl, HEq.refl, and assumption. It also tries to apply heq_of_eq.

Instances For
    source
    def Lean.MVarId.congr? (mvarId : Lean.MVarId) :
    Lean.MetaM (Option (List Lean.MVarId))

    Try to apply a simp congruence theorem.

    Instances For
      source
      def Lean.MVarId.hcongr? (mvarId : Lean.MVarId) :
      Lean.MetaM (Option (List Lean.MVarId))

      Try to apply a hcongr congruence theorem, and then tries to close resulting goals using Eq.refl, HEq.refl, and assumption.

      Instances For
        source
        def Lean.MVarId.congrImplies? (mvarId : Lean.MVarId) :
        Lean.MetaM (Option (List Lean.MVarId))

        Try to apply implies_congr.

        Instances For
          source
          def Lean.MVarId.congrCore (mvarId : Lean.MVarId) :
          Lean.MetaM (List Lean.MVarId)

          Given a goal of the form ⊢ f as = f bs, ⊢ (p → q) = (p' → q'), or ⊢ HEq (f as) (f bs), try to apply congruence. It takes proof irrelevance into account, and the fact that Decidable p is a subsingleton.

          Instances For
            source
            def Lean.MVarId.congrN (mvarId : Lean.MVarId) (depth : optParam Nat 1000000) (closePre : optParam Bool true) (closePost : optParam Bool true) :
            Lean.MetaM (List Lean.MVarId)

            Given a goal of the form ⊢ f as = f bs, ⊢ (p → q) = (p' → q'), or ⊢ HEq (f as) (f bs), try to apply congruence. It takes proof irrelevance into account, and the fact that Decidable p is a subsingleton.

            • Applies congr recursively up to depth depth.
            • If closePre := true, it will attempt to close new goals using Eq.refl, HEq.refl, and assumption with reducible transparency.
            • If closePost := true, it will try again on goals on which congr failed to make progress with default transparency.
            Instances For
              source
              def Lean.MVarId.congrN.post (closePost : optParam Bool true) (mvarId : Lean.MVarId) :
              StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
              Instances For
                source
                def Lean.MVarId.congrN.go (closePre : optParam Bool true) (closePost : optParam Bool true) (n : Nat) (mvarId : Lean.MVarId) :
                StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For