From bf73a26d6a16c24bd9e0252283120e897e929667 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Jul 2024 11:51:47 -0700 Subject: [PATCH] chore: `Simp.Config.implicitDefEqProofs := true` by default Motivation: unblock PR #4595 `Simp.Config.implicitDefEqProofs := false` is currently creating too many issues in Mathlib. --- src/Init/MetaTypes.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index d5b20817118a..1f0b52cc6e77 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -219,13 +219,13 @@ structure Config where -/ index : Bool := true /-- - When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated + When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated with an `rfl`-theorem. Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`. If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp` will **not** create a proof term which is an application of the annotated theorem. -/ - implicitDefEqProofs : Bool := false + implicitDefEqProofs : Bool := true deriving Inhabited, BEq -- Configuration object for `simp_all`