fix: Option.getD eagerly evaluates dflt

src/Init/Prelude.lean

@@ -2213,9 +2213,10 @@ returns `a` if `opt = some a` and `dflt` otherwise.
 This function is `@[macro_inline]`, so `dflt` will not be evaluated unless
 `opt` turns out to be `none`.
 -/
-@[macro_inline] def Option.getD : Option α → α → α
-  | some x, _ => x
-  | none,   e => e
+@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
+  match opt with
+  | some x => x
+  | none => dflt
 
 /--
 Map a function over an `Option` by applying the function to the contained

tests/lean/run/optionGetD.lean

@@ -0,0 +1,12 @@
+import Lean.Data.HashMap
+
+def test (m : Lean.HashMap Nat Nat) : IO (Nat × Nat) := do
+  let start := 1
+  let mut i := start
+  let mut count := 0
+  while i != 0 do
+    i := (m.find? i).getD (panic! "key is not in the map")
+    count := count + 1
+  return (i, count)
+
+#eval test (.ofList [(1,3),(3,2),(2,0)])

tests/lean/smartUnfoldingMatch.lean.expected.out

@@ -1,4 +1,4 @@
 42
-[Meta.debug] r: match x, 0 with
-    | some x, x_1 => x
-    | none, e => e
+[Meta.debug] r: match x with
+    | some x => x
+    | none => 0