Documentation
Batteries
.
Lean
.
Delaborator
Search
Google site search
return to top
source
Imports
Init
Lean.PrettyPrinter
Imported by
Lean
.
ppConst
source
@[deprecated Lean.MessageData.ofConst]
def
Lean
.
ppConst
(e :
Lean.Expr
)
:
Lean.MessageData
Abbreviation for
Lean.MessageData.ofConst
.
Equations
Lean.ppConst
e
=
Lean.MessageData.ofConst
e
Instances For