| changeset 1400 | 5d909faf0e04 |
| parent 1376 | 92f83b9d17e1 |
| child 1557 | fe30812f5b5e |
| 1399:1f00494e37a5 | 1400:5d909faf0e04 |
|---|---|
13 consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) |
13 consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) |
14 |
14 |
15 defs |
15 defs |
16 bind_def "m bind f == case m of Ok r => f r | Fail => Fail" |
16 bind_def "m bind f == case m of Ok r => f r | Fail => Fail" |
17 |
17 |
18 syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) |
|
19 translations "P := E; F" == "E bind (%P.F)" |
|
20 |
|
18 end |
21 end |