diff options
| author | Brian Campbell | 2018-06-20 13:20:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-20 18:21:27 +0100 |
| commit | c2ce7fa6db14551fa49e1d7b46f795bd629c2061 (patch) | |
| tree | 422d38b945e99bf0ce2c2b2a2b4b52b2a137b32e /lib/flow.sail | |
| parent | 7ef315c49caa8b781891d64edc54a7a1ffc010fd (diff) | |
Coq: port handling of effectful and/or from Lem backend
Diffstat (limited to 'lib/flow.sail')
| -rw-r--r-- | lib/flow.sail | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/flow.sail b/lib/flow.sail index 7dc5969e..b698b597 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -2,6 +2,8 @@ $ifndef _FLOW $define _FLOW val not_bool = {coq: "negb", _: "not"} : bool -> bool +/* NB: There are special cases in Sail for effectful uses of and_bool and + or_bool that are not shown here. */ val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool |