diff options
| author | Alasdair Armstrong | 2018-02-05 23:00:58 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-02-05 23:00:58 +0000 |
| commit | fc5ad2e3930b06a8bd382639361b31bd7407f395 (patch) | |
| tree | 9c4b5064cde7fa7fa0027c090e6b654549fbdb63 /lib/flow.sail | |
| parent | 17265a95407c62e78bb850c0e6ffb0876c85c5cb (diff) | |
| parent | bdfcb327ccf23982ae74549fc56ec3451c493ed5 (diff) | |
Merge changes to type_check.ml
Diffstat (limited to 'lib/flow.sail')
| -rw-r--r-- | lib/flow.sail | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/lib/flow.sail b/lib/flow.sail index cb7b1b99..52c98753 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -5,7 +5,7 @@ val not_bool = "not" : bool -> bool val and_bool = "and_bool" : (bool, bool) -> bool val or_bool = "or_bool" : (bool, bool) -> bool -val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -25,6 +25,16 @@ val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> boo val gt_atom_range = "gt" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val eq_range = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool +val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool + +val lteq_int = "lteq" : (int, int) -> bool +val gteq_int = "gteq" : (int, int) -> bool +val lt_int = "lt" : (int, int) -> bool +val gt_int = "lt" : (int, int) -> bool + +overload operator == = {eq_atom, eq_range, eq_int} + $ifdef TEST val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit |