src/HOL/Library/Monad_Syntax.thy
changeset 77107 4c4d40913900
parent 70433 2137db107788
child 80768 c7723cc15de8
equal deleted inserted replaced
77106:5ef443fa4a5d 77107:4c4d40913900
     9   imports Adhoc_Overloading
     9   imports Adhoc_Overloading
    10 begin
    10 begin
    11 
    11 
    12 text \<open>
    12 text \<open>
    13 We provide a convenient do-notation for monadic expressions well-known from Haskell.
    13 We provide a convenient do-notation for monadic expressions well-known from Haskell.
    14 const>\<open>Let\<close> is printed specially in do-expressions.
    14 \<^const>\<open>Let\<close> is printed specially in do-expressions.
    15 \<close>
    15 \<close>
    16 
    16 
    17 consts
    17 consts
    18   bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
    18   bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
    19 
    19