diff options
| author | Thomas Bauereiss | 2020-03-25 20:40:59 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-04-10 13:22:11 +0100 |
| commit | 7bf9b460d3b2c324b4fae8e14e0a54e354002f54 (patch) | |
| tree | 0b499d1b6e4f5081726d85d04fbb66c30e2ddafc /lib | |
| parent | 319c382fe396886fd2b1bd8295c55aa0d9dd0acd (diff) | |
Add Lem builtins for operations on reals
... that match the names in lib/real.sail.
Also fix the lem mapping for abs_int_atom and a Lem syntax error with
nested record updates.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/smt.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/smt.sail b/lib/smt.sail index 93fe0827..2e72e791 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -23,7 +23,7 @@ val emod_int = { val abs_int_atom = { ocaml: "abs_int", interpreter: "abs_int", - lem: "abs_int", + lem: "integerAbs", c: "abs_int", coq: "abs_with_eq" } : forall 'n. int('n) -> int(abs('n)) |