From 14039942f31fb0beebbd0bf336c2be62ff7e2812 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Sat, 10 Jan 2026 14:50:15 +1100 Subject: [PATCH] refactor: derive BEq for Option earlier in import chain (#11960) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR moves the `deriving instance BEq for Option` from `Init.Data.Option.Basic` to `Init.Core`, making `BEq (Option α)` available earlier in the import chain. This is preparatory work for adding `maxSuggestions : Option Nat` fields to `Grind.Config` and `Simp.Config`, which need `BEq (Option Nat)` for the `deriving BEq` clause. The duplicate derivation in `Init.Data.Option.Basic` is kept because proofs there need the definition to be exposed. 🤖 Prepared with Claude Code Co-authored-by: Claude --- src/Init/Core.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 5789c80a06..6103dc6e6d 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -13,6 +13,10 @@ public import Init.SizeOf public section set_option linter.missingDocs true -- keep it documented +-- BEq instance for Option defined here so it's available early in the import chain +-- (before Init.Grind.Config and Init.MetaTypes which need BEq (Option Nat)) +deriving instance BEq for Option + @[expose] section universe u v w