def Lean.Meta.substCore (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) (symm : Bool := false) (fvarSubst : Lean.Meta.FVarSubst := { map := ∅ }) (clearH : Bool := true) (tryToSkip : Bool := false) : Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId)

Equations

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

def Lean.Meta.heqToEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (tryToClear : Bool := true) : Lean.MetaM (Lean.FVarId × Lean.MVarId)

Given h : HEq α a α b in the given goal, produce a new goal where h : Eq α a b. If h is not of the give form, then just return (h, mvarId)

Equations

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

def Lean.Meta.substVar (mvarId : Lean.MVarId) (x : Lean.FVarId) : Lean.MetaM Lean.MVarId

Given x, try to find an equation of the form heq : x = rhs or heq : lhs = x, and runs substCore on it. Throws an exception if no such equation is found.

Equations

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

partial def Lean.Meta.subst (mvarId : Lean.MVarId) (h : Lean.FVarId) : Lean.MetaM Lean.MVarId

def Lean.Meta.subst.substEq (mvarId : Lean.MVarId) (h : Lean.FVarId) : Lean.MetaM Lean.MVarId

Give h : Eq α a b, try to apply substCore

Equations

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

def Lean.Meta.substVar? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) : Lean.MetaM (Option Lean.MVarId)

Given x, try to find an equation of the form heq : x = rhs or heq : lhs = x, and runs substCore on it. Returns none if no such equation is found, or if substCore fails.

Equations

• Lean.Meta.substVar? mvarId hFVarId = Lean.observing? (Lean.Meta.substVar mvarId hFVarId)

def Lean.Meta.subst? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

• Lean.Meta.subst? mvarId hFVarId = Lean.observing? (Lean.Meta.subst mvarId hFVarId)

def Lean.Meta.substCore? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) (symm : Bool := false) (fvarSubst : Lean.Meta.FVarSubst := { map := ∅ }) (clearH : Bool := true) (tryToSkip : Bool := false) : Lean.MetaM (Option (Lean.Meta.FVarSubst × Lean.MVarId))

Equations

• Lean.Meta.substCore? mvarId hFVarId symm fvarSubst clearH tryToSkip = Lean.observing? (Lean.Meta.substCore mvarId hFVarId symm fvarSubst clearH tryToSkip)

def Lean.Meta.trySubstVar (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.trySubstVar mvarId hFVarId = do let __do_lift ← Lean.Meta.substVar? mvarId hFVarId pure (__do_lift.getD mvarId)

def Lean.Meta.trySubst (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.trySubst mvarId hFVarId = do let __do_lift ← Lean.Meta.subst? mvarId hFVarId pure (__do_lift.getD mvarId)

def Lean.Meta.substSomeVar? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

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

partial def Lean.Meta.substVars (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId