From 10982cd94da2f7983a7a93c655e2f43ec8d57bdc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Mar 2018 17:57:27 +0100 Subject: [PATCH] chore(init/category/lift): document monad_run --- library/init/category/lift.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/init/category/lift.lean b/library/init/category/lift.lean index 6b15a5bc53..9f1cb67c7c 100644 --- a/library/init/category/lift.lean +++ b/library/init/category/lift.lean @@ -53,7 +53,9 @@ instance monad_functor_t_refl (m m') : monad_functor_t m m' m m' := @[simp] lemma monad_map_refl {m m' : Type u → Type v} (f : ∀ {α}, m α → m' α) {α} : (monad_map @f : m α → m' α) = f := rfl -/-- Run a monad stack to completion. -/ +/-- Run a monad stack to completion. + `run` should be the composition of the transformers' individual `run` functions. + `unrun` should be its inverse. -/ class monad_run (out : out_param $ Type u → Type v) (m : Type u → Type v) := (run {} {α : Type u} : m α → out α) (unrun {} {α : Type u} : out α → m α)