diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean
index fb41d87707f5..2d174804d645 100644
--- a/src/Lean/Util/LeanOptions.lean
+++ b/src/Lean/Util/LeanOptions.lean
@@ -43,6 +43,9 @@ instance : Coe Bool LeanOptionValue where
 instance : Coe Nat LeanOptionValue where
   coe := LeanOptionValue.ofNat
 
+instance {n : Nat} : OfNat LeanOptionValue n where
+  ofNat := .ofNat n
+
 instance : FromJson LeanOptionValue where
   fromJson?
     | (s : String) => Except.ok s