Bundled monads

BundledMonad packages a Type u → Type v constructor with a Monad instance so it can be stored inside inductive types (e.g. per-node monad decorations) where typeclass inference is not available. This module is independent of Interaction.Spec.

structure BundledMonad : Type (max (u + 1) (v + 1))

Bundled monad: a monad constructor packaged as a structure for use inside Spec data.

• M : Type u → Type v

  The underlying monad family.

• inst : Monad self.M

  Witness that M has a Monad instance.

@[implicit_reducible]

instance BundledMonad.instMonad (bm : BundledMonad) : Monad bm.M