From f2abe87ddf4f78ee2b4bc1f610f358a748a76f7b Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Thu, 15 Sep 2022 18:39:22 +0200 Subject: [PATCH] chore: fix a typo in def name getOptionDefaulValue renamed to getOptionDefaultValue --- src/Lean/Data/Options.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 21a94a1ff3..70bebf93ff 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -51,7 +51,7 @@ def getOptionDecl (name : Name) : IO OptionDecl := do let (some decl) ← pure (decls.find? name) | throw $ IO.userError s!"unknown option '{name}'" pure decl -def getOptionDefaulValue (name : Name) : IO DataValue := do +def getOptionDefaultValue (name : Name) : IO DataValue := do let decl ← getOptionDecl name pure decl.defValue @@ -63,7 +63,7 @@ def setOptionFromString (opts : Options) (entry : String) : IO Options := do let ps := (entry.splitOn "=").map String.trim let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form ' = '" let key := Name.mkSimple key - let defValue ← getOptionDefaulValue key + let defValue ← getOptionDefaultValue key match defValue with | DataValue.ofString _ => pure $ opts.setString key val | DataValue.ofBool _ =>