structure Lean.Meta.UnifyEqResult : Type

• mvarId : MVarId
• subst : FVarSubst
• numNewEqs : Nat

def Lean.Meta.unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := { map := ∅ }) (acyclic : MVarId → Expr → MetaM Bool := fun (x : MVarId) (x : Expr) => pure false) (caseName? : Option Name := none) : MetaM (Option UnifyEqResult)

Helper method for methods such as Cases.unifyEqs?. Given the given goal mvarId containing the local hypothesis eqFVarId, it performs the following operations:

• If eqFVarId is a heterogeneous equality, tries to convert it to a homogeneous one.
• If eqFVarId is a homogeneous equality of the form a = b, it tries
  • If a and b are definitionally equal, clear it
  • Normalize a and b using the current reducibility setting.
  • If a (b) is a free variable not occurring in b (a), replace it everywhere.
  • If a and b are distinct constructors, return none to indicate that the goal has been closed.
  • If a and b are the same constructor, apply injection, the result contains the number of new equalities introduced in the goal.
  • It also tries to apply the given acyclic method to try to close the goal. Remark: It is a parameter because simp uses unifyEq?, and acyclic depends on simp.

Equations

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

def Lean.Meta.unifyEq?.substEq (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := { map := ∅ }) (acyclic : MVarId → Expr → MetaM Bool := fun (x : MVarId) (x : Expr) => pure false) (eqDecl : LocalDecl) (a b : Expr) (symm : Bool) : MetaM (Option UnifyEqResult)

Equations

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

def Lean.Meta.unifyEq?.injection (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := { map := ∅ }) (caseName? : Option Name := none) (eqDecl : LocalDecl) (injectionOffset? : Expr → Expr → MetaM (Option MVarId)) (a b : Expr) : MetaM (Option UnifyEqResult)

Equations

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