source
structure Lean.Meta.UnifyEqResult :
Type

- mvarId : MVarId
- subst : FVarSubst
- numNewEqs : Nat

Instances For

source
def Lean.Meta.unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := { }) (acyclic : MVarId → Expr → MetaM Bool := fun (x : MVarId) (x_1 : 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.

Instances For