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) :
Equations
Equations
Equations
Equations
Equations