From 08d8a0873e2c4409d7bb67b0f0a5798df2f7ada2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 17 Oct 2024 11:38:52 +0200 Subject: [PATCH] doc: remove docstring from implicitDefEqProofs (#5751) this option was added in fb97275dcbb683efe6da87ed10a3f0cd064b88fd to prepare for #4595, due to boostrapping issues, but #4595 has not landed yet. This is be very confusing when people discover this option and try to use it (as I did). So let's clearly mark this as not yet implemented on `master`, and add the docstring only with #4595. --- src/Init/MetaTypes.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 06e8f37f74..aa7ade2488 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -224,11 +224,7 @@ structure Config where -/ index : Bool := true /-- - 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. + This option does not have any effect (yet). -/ implicitDefEqProofs : Bool := true deriving Inhabited, BEq