From fb97275dcbb683efe6da87ed10a3f0cd064b88fd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Jun 2024 09:29:17 -0700 Subject: [PATCH] feat: add `Simp.Config.implicitDefEqProofs` This commit does **not** implement this feature. --- src/Init/MetaTypes.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index e4cf1f09c6..d5b2081711 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -218,6 +218,14 @@ structure Config where to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior. -/ index : Bool := true + /-- + When `true` (default: `false`), `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 deriving Inhabited, BEq -- Configuration object for `simp_all`