def Lean.MVarId.congrPre (mvarId : MVarId) : MetaM (Option 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.

Equations

• One or more equations did not get rendered due to their size.

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

Try to apply a simp congruence theorem.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.hcongr? (mvarId : MVarId) : MetaM (Option (List 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.

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

Try to apply implies_congr.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.congrCore (mvarId : MVarId) : MetaM (List MVarId)

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.congrN (mvarId : MVarId) (depth : Nat := 1000000) (closePre closePost : Bool := true) : MetaM (List MVarId)

Given a goal of the form ⊢ f as = f bs, ⊢ (p → q) = (p' → q'), or ⊢ 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

• mvarId.congrN depth closePre closePost = do let __discr ← (Lean.MVarId.congrN.go✝ closePre closePost depth mvarId).run #[] match __discr with | (fst, s) => pure s.toList