def
Lean.Meta.ppGoal.pushPending
(indent : Int)
(ids : List Lake.Name)
(type? : Option Lean.Expr)
(fmt : Lean.Format)
:
Instances For
def
Lean.Meta.ppGoal.ppVars
(indent : Int)
(showLetValues : Bool)
(varNames : List Lake.Name)
(prevType? : Option Lean.Expr)
(fmt : Lean.Format)
(localDecl : Lean.LocalDecl)
: