Documentation

Lean.Meta.Tactic.Subst

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

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.subst.findEq (mvarId : Lean.MVarId) (h : Lean.FVarId) :

Lean.MetaM Lean.MVarId

Try to find an equation of the form heq : h = rhs or heq : lhs = h

Equations

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

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 : optParam Bool false) (fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ }) (clearH : optParam Bool true) (tryToSkip : optParam 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.trySubst (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.trySubst mvarId hFVarId = do let a ← Lean.Meta.subst? mvarId hFVarId match a with | some mvarId => pure mvarId | none => pure 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