From b28ff947803a85cf8772d13193c3bbb4cbdd57d3 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 6 May 2017 02:29:56 -0400 Subject: [PATCH] feat(init/data/option_t): option_t is a monad transformer --- library/init/data/option_t.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/library/init/data/option_t.lean b/library/init/data/option_t.lean index 3f572a02c8..e2ad667565 100644 --- a/library/init/data/option_t.lean +++ b/library/init/data/option_t.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.meta.interactive +import init.meta.interactive init.category.transformers universes u v @@ -66,3 +66,7 @@ instance {m : Type u → Type v} [monad m] : alternative (option_t m) := def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (a : m α) : option_t m α := (some <$> a : m (option α)) + +instance option_t.monad_transformer : monad.monad_transformer option_t := +{ is_monad := @option_t.monad, + monad_lift := @option_t.lift }