From d2f4ce0158fbf228200201e4ddfdc69e4613415a Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 10 Apr 2025 16:49:03 +0200 Subject: [PATCH] fix: Add `Inhabited` instance for `OptionT` (#7901) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds `instance [Pure f] : Inhabited (OptionT f α)`, so that `Inhabited (OptionT Id Empty)` synthesizes. Co-authored-by: Sebastian Graf --- src/Init/Control/Option.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index 4f80137b99..c7ae74dc55 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -59,6 +59,9 @@ instance : Monad (OptionT m) where pure := OptionT.pure bind := OptionT.bind +instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where + default := pure (f:=m) default + /-- Recovers from failures. Typically used via the `<|>` operator. -/