| changeset 62505 | 9e2a65912111 |
| parent 61845 | c5c7bc41185c |
| child 78062 | edb195122938 |
| 62504:f14f17e656a6 | 62505:9e2a65912111 |
|---|---|
100 |
100 |
101 |
101 |
102 (* partiality *) |
102 (* partiality *) |
103 |
103 |
104 fun try f x = SOME (f x) |
104 fun try f x = SOME (f x) |
105 handle exn => if Exn.is_interrupt exn then reraise exn else NONE; |
105 handle exn => if Exn.is_interrupt exn then Exn.reraise exn else NONE; |
106 |
106 |
107 fun can f x = is_some (try f x); |
107 fun can f x = is_some (try f x); |
108 |
108 |
109 |
109 |
110 (* lists *) |
110 (* lists *) |