diff options
| author | Alasdair | 2019-04-27 00:20:37 +0100 |
|---|---|---|
| committer | Alasdair | 2019-04-27 00:40:56 +0100 |
| commit | 0c99f19b012205f1be1d4ae18b722ecbdd80e3d4 (patch) | |
| tree | 55f796f9bdf270064bfe87bdf275b93ffcdc1fb2 /lib/smt.sail | |
| parent | bf240119e43cb4e3b5f5746b5ef21f19a8fac2d2 (diff) | |
| parent | 094c8e254abde44d45097aca7a36203704fe2ef4 (diff) | |
Merge branch 'sail2' into smt_experiments
Diffstat (limited to 'lib/smt.sail')
| -rw-r--r-- | lib/smt.sail | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/smt.sail b/lib/smt.sail index 4d250bef..f58c008f 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -6,6 +6,7 @@ $define _SMT /*! Euclidean division */ val ediv_int = { ocaml: "quotient", + interpreter: "quotient", lem: "integerDiv", c: "ediv_int", coq: "ediv_with_eq" @@ -13,6 +14,7 @@ val ediv_int = { val emod_int = { ocaml: "modulus", + interpreter: "modulus", lem: "integerMod", c: "emod_int", coq: "emod_with_eq" @@ -20,6 +22,7 @@ val emod_int = { val abs_int = { ocaml: "abs_int", + interpreter: "abs_int", lem: "abs_int", c: "abs_int", coq: "abs_with_eq" |