diff --git a/library/init/default.lean b/library/init/default.lean index 1f7bcbb7d0..4c3570cfc4 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -8,3 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic import init.relation init.wf init.nat init.wf_k init.prod import init.bool init.num init.sigma init.measurable init.setoid init.quot import init.funext init.function init.subtype init.classical init.simplifier +import init.monad diff --git a/library/init/functor.lean b/library/init/functor.lean new file mode 100644 index 0000000000..cafc7a7bf0 --- /dev/null +++ b/library/init/functor.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) Luke Nelson and Jared Roesch. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Luke Nelson and Jared Roesch +-/ +prelude + +structure functor [class] (f : Type → Type) : Type := +(map : Π {a b: Type}, (a → b) → f a → f b) diff --git a/library/init/monad.lean b/library/init/monad.lean new file mode 100644 index 0000000000..287a978628 --- /dev/null +++ b/library/init/monad.lean @@ -0,0 +1,11 @@ +/- +Copyright (c) Luke Nelson and Jared Roesch. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Luke Nelson and Jared Roesch +-/ +prelude +import init.functor + +structure monad [class] (m : Type → Type) extends functor m : Type := +(return : Π {a:Type}, a → m a) +(bind : Π {a b: Type}, m a → (a → m b) → m b)