diff options
| author | Brian Campbell | 2018-07-12 15:36:33 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-12 15:36:33 +0100 |
| commit | 3e8afd335d1648b700fa04c80312326aec49c9c0 (patch) | |
| tree | 389033a1683995ffef532f67641e13ba17b23d6b /lib/flow.sail | |
| parent | f3d480d3fee8c28c1dd1975117149ddcd47d989f (diff) | |
Coq: handle all bool conjunctions/disjunctions
Diffstat (limited to 'lib/flow.sail')
| -rw-r--r-- | lib/flow.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flow.sail b/lib/flow.sail index 304f14bc..b4440eaa 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -9,7 +9,7 @@ val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool -val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool function neq_atom (x, y) = not_bool(eq_atom(x, y)) |