diff options
| author | Thomas Bauereiss | 2017-07-15 18:29:45 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-07-15 18:57:55 +0100 |
| commit | 0a3d703f8180cb0163a6e0d26f0bce198ae221db (patch) | |
| tree | 15b5900710945cf92ffbed073c52af954e6b3e12 /src/util.ml | |
| parent | c63f9086a721c902c2b5c170758c7c63f02330f8 (diff) | |
Add version of rewriter for new typechecker
Diffstat (limited to 'src/util.ml')
| -rw-r--r-- | src/util.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/util.ml b/src/util.ml index 9b76c118..d2d4eea7 100644 --- a/src/util.ml +++ b/src/util.ml @@ -203,6 +203,12 @@ let option_bind f = function | None -> None | Some(o) -> f o +let rec option_binop f x y = match x, y with + | None, None -> None + | Some x, None -> Some x + | None, Some y -> Some y + | Some x, Some y -> Some (f x y) + let changed2 f g x h y = match (g x, h y) with | (None,None) -> None |