diff options
| author | Robert Norton | 2018-07-12 17:04:40 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-07-12 17:05:19 +0100 |
| commit | 3c4a27d7041d71fb229970dacab013cf84669755 (patch) | |
| tree | 390447236c61e7de0d4f6bbaae9276635edc72d6 /mips/prelude.sail | |
| parent | e6977ee8e2ba7a53d69f2fb3b715846a62a50454 (diff) | |
Add missing builtins needed for cheri128 C. Still doesn't build possibly due to code gen issue.
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index 85060dda..4c77d522 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -116,9 +116,9 @@ val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int -val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} +val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} -val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} +val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom", c:"max_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} overload min = {min_atom, min_nat, min_int} |