Documentation

Lean.Meta.PPGoal

def Lean.Meta.withPPInaccessibleNamesImp {α : Type} (flag : Bool) (x : Lean.MetaM α) :
Equations
def Lean.Meta.withPPInaccessibleNames {m : TypeType u_1} {α : Type} [inst : MonadControlT Lean.MetaM m] [inst : Monad m] (x : m α) (flag : optParam Bool true) :
m α
Equations
structure Lean.Meta.ToHide.State :
Type
structure Lean.Meta.ToHide.Context :
Type
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
def Lean.Meta.ppGoal.ppVars (indent : Int) (hiddenProp : Lean.FVarIdSet) (varNames : List Lean.Name) (prevType? : Option Lean.Expr) (fmt : Lean.Format) (localDecl : Lean.LocalDecl) :
Equations