From c4ff5fe19914099dff571a4c74cc20f4247ab207 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 27 Nov 2022 08:31:33 +1100 Subject: [PATCH] chore: change simp default to decide := false --- src/Init/Meta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 533fc8f809..5dbd30f84d 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1218,7 +1218,7 @@ structure Config where etaStruct : EtaStructMode := .all iota : Bool := true proj : Bool := true - decide : Bool := true + decide : Bool := false autoUnfold : Bool := false deriving Inhabited, BEq, Repr