Theory Pure_Monad

section ‹Monadification›

subsection ‹Monads›

theory Pure_Monad
  imports Main
begin

definition Wrap :: "'a  'a" where
  "Wrap x  x"

definition App :: "('a  'b)  'a  'b" where
  "App f  f"

lemma Wrap_App_Wrap:
  "App (Wrap f) (Wrap x)  f x"
  unfolding App_def Wrap_def .


end