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

fix: undefined symbol without LEAN_USE_GMP (#9106)

Browse source 
This PR fixes `undefined symbol: lean::mpz::divexact(lean::mpz const&,
lean::mpz const&)` when building without `LEAN_USE_GMP`

This fixes a regression in #8089
This commit is contained in:
Eric Wieser 2025-07-03 17:50:21 +01:00 • committed by GitHub
parent ba7135d73c
commit 0106ca3bec
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/runtime/mpz.cpp
View file

@ -763,7 +763,7 @@ mpz & mpz::operator%=(mpz const & o) {
return rem(o.m_size, o.m_digits);
}
mpz divexact(mpz const & n, mpz const & d) {
mpz mpz::divexact(mpz const & n, mpz const & d) {
return n / d;
}