opaque Lean.Linter.linter.all : Lean.Option Bool

def Lean.Linter.getLinterAll (o : Lean.Options) (defValue : optParam Bool Lean.Linter.linter.all.defValue) : Bool

Equations

• Lean.Linter.getLinterAll o defValue = Lean.KVMap.get o Lean.Linter.linter.all.name defValue

def Lean.Linter.getLinterValue (opt : Lean.Option Bool) (o : Lean.Options) : Bool

Equations

• Lean.Linter.getLinterValue opt o = Lean.KVMap.get o opt.name (Lean.Linter.getLinterAll o opt.defValue)