diff options
Diffstat (limited to 'aarch64_small/prelude.sail')
| -rw-r--r-- | aarch64_small/prelude.sail | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail index a7bc2388..d58158cb 100644 --- a/aarch64_small/prelude.sail +++ b/aarch64_small/prelude.sail @@ -120,8 +120,10 @@ overload operator - = {sub_int, sub_vec, sub_vec_int} /* function reg_index x = unsigned(x) */ -val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat -val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int +val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : + forall 'M 'N, 'M >= 0 & 'N >= 0. (atom('M), atom('N)) -> atom(div('M,'N)) +val quotient = {ocaml: "quotient", lem: "integerDiv"} : + forall 'M 'N. (atom('M), atom('N)) -> atom(div('M,'N)) overload quot = {quotient_nat, quotient} |