Documentation

Lean.Meta.Tactic.Congr

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.

Equations
    Instances For

      Try to apply a simp congruence theorem.

      Equations
        Instances For

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

          Equations
            Instances For

              Try to apply implies_congr.

              Equations
                Instances For

                  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.

                  Equations
                    Instances For
                      def Lean.MVarId.congrN (mvarId : MVarId) (depth : Nat := 1000000) (closePre closePost : Bool := true) :

                      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.
                      Equations
                        Instances For
                          Equations
                            Instances For
                              def Lean.MVarId.congrN.go (closePre closePost : Bool := true) (n : Nat) (mvarId : MVarId) :
                              Equations
                                Instances For