equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Monad notation for arbitrary types *} |
5 header {* Monad notation for arbitrary types *} |
6 |
6 |
7 theory Monad_Syntax |
7 theory Monad_Syntax |
8 imports Main "~~/src/Tools/Adhoc_Overloading" |
8 imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List" |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 We provide a convenient do-notation for monadic expressions |
12 We provide a convenient do-notation for monadic expressions |
13 well-known from Haskell. @{const Let} is printed |
13 well-known from Haskell. @{const Let} is printed |
71 |
71 |
72 setup {* |
72 setup {* |
73 Adhoc_Overloading.add_overloaded @{const_name bind} |
73 Adhoc_Overloading.add_overloaded @{const_name bind} |
74 #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind} |
74 #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind} |
75 #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind} |
75 #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind} |
|
76 #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind} |
76 *} |
77 *} |
77 |
78 |
78 end |
79 end |