fix: uses PUnit, pure () forces implicit universe parameter to be 1

Remark: we should probably elaborate `def`s like we elaborate theorems when the resulting type is provided.
2026-03-18 10:54:09 +00:00 · 2024-06-07 16:05:25 -07:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@@ -72,7 +72,7 @@ satisfy `p`, using the proof to apply `f`.

 /-- Map a monadic function which returns `Unit` over an `Option`. -/
@[inline] protected def forM [Pure m] : Option α → (α → m PUnit) → m PUnit
-  | none  , _ => pure ()
+  | none  , _ => pure ⟨⟩
  | some a, f => f a

 instance : ForM m (Option α) α :=