| changeset 22936 | 284b56463da8 |
| parent 22935 | c6689e15bc98 |
| child 23225 | 591af6a2f09e |
| 22935:c6689e15bc98 | 22936:284b56463da8 |
|---|---|
70 |
70 |
71 (*result views*) |
71 (*result views*) |
72 fun `f = fn x => (f x, x); |
72 fun `f = fn x => (f x, x); |
73 fun tap f = fn x => (f x; x); |
73 fun tap f = fn x => (f x; x); |
74 |
74 |
75 fun flip f x y = f y x |
75 fun flip f x y = f y x; |
76 |
|
76 |
77 |
77 (* options *) |
78 (* options *) |
78 |
79 |
79 fun is_some (SOME _) = true |
80 fun is_some (SOME _) = true |
80 | is_some NONE = false; |
81 | is_some NONE = false; |