Documentation

Lean.Meta.Tactic.UnifyEq

Instances For
    def Lean.Meta.unifyEq? (mvarId : Lean.MVarId) (eqFVarId : Lean.FVarId) (subst : optParam Lean.Meta.FVarSubst { map := }) (acyclic : optParam (Lean.MVarIdLean.ExprLean.MetaM Bool) fun x x => pure false) (caseName? : optParam (Option Lake.Name) none) :

    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 contructor, 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
      def Lean.Meta.unifyEq?.substEq (mvarId : Lean.MVarId) (eqFVarId : Lean.FVarId) (subst : optParam Lean.Meta.FVarSubst { map := }) (acyclic : optParam (Lean.MVarIdLean.ExprLean.MetaM Bool) fun x x => pure false) (eqDecl : Lean.LocalDecl) (a : Lean.Expr) (b : Lean.Expr) (symm : Bool) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For