Monadic bind is now infixl as is the norm
authornipkow
Mon Jul 29 14:28:30 2019 +0200 (3 weeks ago ago)
changeset 706182137db107788
parent 70617 495881aadbff
child 70620 4abd07cd034f
Monadic bind is now infixl as is the norm
src/HOL/Library/Monad_Syntax.thy
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Sun Jul 28 15:39:30 2019 +0200
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Mon Jul 29 14:28:30 2019 +0200
     1.3 @@ -10,27 +10,26 @@
     1.4  begin
     1.5  
     1.6  text \<open>
     1.7 -  We provide a convenient do-notation for monadic expressions
     1.8 -  well-known from Haskell.  \<^const>\<open>Let\<close> is printed
     1.9 -  specially in do-expressions.
    1.10 +We provide a convenient do-notation for monadic expressions well-known from Haskell.
    1.11 +const>\<open>Let\<close> is printed specially in do-expressions.
    1.12  \<close>
    1.13  
    1.14  consts
    1.15 -  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
    1.16 +  bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
    1.17  
    1.18  notation (ASCII)
    1.19 -  bind (infixr ">>=" 54)
    1.20 +  bind (infixl ">>=" 54)
    1.21  
    1.22  
    1.23  abbreviation (do_notation)
    1.24 -  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
    1.25 +  bind_do :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd"
    1.26    where "bind_do \<equiv> bind"
    1.27  
    1.28  notation (output)
    1.29 -  bind_do (infixr "\<bind>" 54)
    1.30 +  bind_do (infixl "\<bind>" 54)
    1.31  
    1.32  notation (ASCII output)
    1.33 -  bind_do (infixr ">>=" 54)
    1.34 +  bind_do (infixl ">>=" 54)
    1.35  
    1.36  
    1.37  nonterminal do_binds and do_bind
    1.38 @@ -41,11 +40,11 @@
    1.39    "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    1.40    "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    1.41    "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    1.42 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
    1.43 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl "\<then>" 54)
    1.44  
    1.45  syntax (ASCII)
    1.46    "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
    1.47 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    1.48 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
    1.49  
    1.50  translations
    1.51    "_do_block (_do_cons (_do_then t) (_do_final e))"