equal
deleted
inserted
replaced
13 constdefs |
13 constdefs |
14 bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) |
14 bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) |
15 "m bind f == case m of Ok r => f r | Fail => Fail" |
15 "m bind f == case m of Ok r => f r | Fail => Fail" |
16 |
16 |
17 syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) |
17 syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) |
18 translations "P := E; F" == "E bind (%P.F)" |
18 translations "P := E; F" == "E bind (%P. F)" |
19 |
19 |
20 end |
20 end |