Documentation

Lean.Meta.Tactic.Congr

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

Try to apply a simp congruence theorem.

Equations
  • One or more equations did not get rendered due to their size.
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.congrImplies? (mvarId : Lean.MVarId) :
Lean.MetaM (Option (List Lean.MVarId))

Try to apply implies_congr.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.congr (mvarId : Lean.MVarId) (closeEasy : 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, the fact that Decidable p is a subsingleton. If closeEasy := true, it tries to close new subgoals using Eq.refl, HEq.refl, and assumption.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.congrN (mvarId : Lean.MVarId) (n : Nat) :
Lean.MetaM (List Lean.MVarId)

Applies congr recursively up to depth n.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.congrN.go (n : Nat) (mvarId : Lean.MVarId) :
StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
Equations