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