Theory Monad_Memo_DP.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