equal
deleted
inserted
replaced
8 |
8 |
9 Maybe = List + |
9 Maybe = List + |
10 |
10 |
11 datatype 'a maybe = Ok 'a | Fail |
11 datatype 'a maybe = Ok 'a | Fail |
12 |
12 |
13 consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) |
13 constdefs |
14 |
14 bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) |
15 defs |
15 "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 |
16 |
18 syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) |
17 syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) |
19 translations "P := E; F" == "E bind (%P.F)" |
18 translations "P := E; F" == "E bind (%P.F)" |
20 |
19 |
21 end |
20 end |