From eeedc22724987bf8ec4660739d3140e752236ac1 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 22 Aug 2024 12:46:32 -0400
Subject: [PATCH] feat: `#where` supports weak options

---
 Batteries/Tactic/Where.lean | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/Batteries/Tactic/Where.lean b/Batteries/Tactic/Where.lean
index 7a07d2ba6b..3ef51a46c9 100644
--- a/Batteries/Tactic/Where.lean
+++ b/Batteries/Tactic/Where.lean
@@ -40,10 +40,14 @@ private def describeOpenDecls (ds : List OpenDecl) : MessageData := Id.run do
 
 private def describeOptions (opts : Options) : CommandElabM (Option MessageData) := do
   let mut lines := #[]
+  let decls ← getOptionDecls
   for (name, val) in opts do
-    let dval ← getOptionDefaultValue name
-    if val != dval then
-      lines := lines.push m!"set_option {name} {val}"
+    match decls.find? name with
+    | some decl =>
+      if val != decl.defValue then
+        lines := lines.push m!"set_option {name} {val}"
+    | none =>
+      lines := lines.push m!"-- set_option {name} {val}  -- unknown"
   if lines.isEmpty then
     return none
   else