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

Equations

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

def Lean.Meta.heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool := true) : MetaM (FVarId × 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 : MVarId) (x : FVarId) : MetaM 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 : MVarId) (h : FVarId) : MetaM MVarId

def Lean.Meta.substVar? (mvarId : MVarId) (hFVarId : FVarId) : MetaM (Option 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 : MVarId) (hFVarId : FVarId) : MetaM (Option MVarId)

Equations

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

def Lean.Meta.substCore? (mvarId : MVarId) (hFVarId : FVarId) (symm : Bool := false) (fvarSubst : FVarSubst := { }) (clearH : Bool := true) (tryToSkip : Bool := false) : MetaM (Option (FVarSubst × 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 : MVarId) (hFVarId : FVarId) : MetaM 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 : MVarId) (hFVarId : FVarId) : MetaM 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 : MVarId) : MetaM (Option MVarId)

Equations

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

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