max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-31 08:52:24 -08:00
parent 36e70e9a08
commit 9419b178bc
2 changed files with 15 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/include/lean/lean.h generated
View file

@ -1553,7 +1553,7 @@ static inline lean_obj_res lean_int_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
int v1 = lean_scalar_to_int(a1);
int v2 = lean_scalar_to_int(a2);
if (v2 == 0)
return lean_box(0);
return v1 >= 0 ? a1 : lean_int_to_int(-1 - v1);
else
return lean_int_to_int(v1 % v2);
} else {

18
stage0/src/runtime/object.cpp generated
View file

@ -1340,12 +1340,22 @@ extern "C" object * lean_int_big_div(object * a1, object * a2) {
}
extern "C" object * lean_int_big_mod(object * a1, object * a2) {
if (lean_is_scalar(a1))
if (lean_is_scalar(a1)) {
return mpz_to_int(mpz(lean_scalar_to_int(a1)) % mpz_value(a2));
else if (lean_is_scalar(a2))
return mpz_to_int(mpz_value(a1) % mpz(lean_scalar_to_int(a2)));
else
} else if (lean_is_scalar(a2)) {
int i2 = lean_scalar_to_int(a2);
if (i2 == 0) {
if (mpz_value(a1) >= 0) {
return a1;
} else {
return mpz_to_int(mpz(-1) - mpz_value(a1));
}
} else {
return mpz_to_int(mpz_value(a1) % mpz(i2));
}
} else {
return mpz_to_int(mpz_value(a1) % mpz_value(a2));
}
}
extern "C" bool lean_int_big_eq(object * a1, object * a2) {