From c24b419ee458bc9327574fbd49f55d4addf2b0c5 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 12 Apr 2024 15:02:08 -0700
Subject: [PATCH] doc: fix `simp` configuration option default value for
 `decide` (#3894)

---
 src/Init/MetaTypes.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index 8ba1a2e217..c5832eb4ed 100644
--- a/src/Init/MetaTypes.lean
+++ b/src/Init/MetaTypes.lean
@@ -130,7 +130,7 @@ structure Config where
   -/
   proj              : Bool := true
   /--
-  When `true` (default: `true`), rewrites a proposition `p` to `True` or `False` by inferring
+  When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
   a `Decidable p` instance and reducing it.
   -/
   decide            : Bool := false