From 59bf4defc633af4e4513bd96fec92a97e23c5b33 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Sep 2020 15:58:29 -0700 Subject: [PATCH] fix: default value --- src/Lean/Meta/SynthInstance.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 1fda79f320..9f3e9236c8 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -524,11 +524,11 @@ forallTelescope type $ fun xs typeBody => mkForallFVars xs (mkAppN c args) | _ => pure type +def maxStepsDefault := 1000 @[init] def maxStepsOption : IO Unit := -registerOption `synthInstance.maxSteps { defValue := (1000 : Nat), group := "", descr := "maximum steps for the type class instance synthesis procedure" } - +registerOption `synthInstance.maxSteps { defValue := maxStepsDefault, group := "", descr := "maximum steps for the type class instance synthesis procedure" } private def getMaxSteps (opts : Options) : Nat := -opts.getNat `synthInstance.maxSteps 10000 +opts.getNat `synthInstance.maxSteps maxStepsDefault private def synthInstanceImp? (type : Expr) : MetaM (Option Expr) := do opts ← getOptions;