Documentation
Lean
.
Linter
.
Basic
Search
Google site search
Lean
.
Linter
.
Basic
source
Imports
Init
Lean.Data.Options
Imported by
Lean
.
Linter
.
linter
.
all
Lean
.
Linter
.
getLinterAll
Lean
.
Linter
.
getLinterValue
source
opaque
Lean
.
Linter
.
linter
.
all
:
Lean.Option
Bool
source
def
Lean
.
Linter
.
getLinterAll
(o :
Lean.Options
)
(defValue :
optParam
Bool
Lean.Linter.linter.all
.defValue
)
:
Bool
Instances For
source
def
Lean
.
Linter
.
getLinterValue
(opt :
Lean.Option
Bool
)
(o :
Lean.Options
)
:
Bool
Instances For