From 77dda12bc9144d5ce2fba6e79669fdae543a8d12 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Feb 2022 16:30:44 -0800 Subject: [PATCH] chore: add `Simp.Config.arith` option --- src/Init/Meta.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 84382169d8..222139c82a 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1008,6 +1008,7 @@ structure Config where iota : Bool := true proj : Bool := true decide : Bool := true + arith : Bool := true deriving Inhabited, BEq, Repr -- Configuration object for `simp_all` @@ -1020,7 +1021,8 @@ def neutralConfig : Simp.Config := eta := false iota := false proj := false - decide := false } + decide := false + arith := false } end Simp