max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26496 commits 1 branch 0 tags 5.3 GiB
Commit graph

21 commits

Author SHA1 Message Date
Leonardo de Moura
e9e40789c1 fix: mpz::power for USE_GMP=OFF 2021-11-30 17:57:33 -08:00
Leonardo de Moura
83d6eb1c72 fix: mpz::mul2k for USE_GMP=OFF 2021-11-30 17:19:16 -08:00
Leonardo de Moura
8aca088752 feat: mpz missing methods for USE_GMP=OFF 2021-11-30 16:46:53 -08:00
Leonardo de Moura
e5b3b180dc feat: some mpz methods for LEAN_USE_GMP=OFF 2021-11-29 17:55:04 -08:00
Leonardo de Moura
ec6932fbb7 feat: some mpz methods for LEAN_USE_GMP=OFF 2021-11-29 16:01:07 -08:00
Leonardo de Moura
68fc9a9115 feat: add dummy mpz implementation for LEAN_USE_GMP=OFF 2021-11-29 11:42:08 -08:00
Leonardo de Moura
0002d8bd04 chore: missing #ifdef LEAN_USE_GMP 2021-11-29 11:35:13 -08:00
Leonardo de Moura
6396f3b2c1 chore: simplify mpz.h 
Add basic support for `LEAN_USE_GMP=OFF`.
 2021-11-29 11:11:49 -08:00
Leonardo de Moura
6d0fa6da7c chore: remove mpz dead code 2021-10-26 12:05:19 -07:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Joe Hendrix
9bd60c7519 feat: Nat/Fin/UInt instances of bitwise classes 2021-03-04 15:42:43 -08:00
Leonardo de Moura
2f1ec93289 chore: move runtime implementation to src/runtime 2020-05-22 14:35:16 -07:00
Leonardo de Moura
1a77ee4f89 chore: delete old runtime directory 2020-05-18 11:33:18 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Sebastian Ullrich
9707672cc8 fix(runtime/mpz): fix and document size_t functions 2019-07-05 16:27:04 -07:00
Sebastian Ullrich
2c9dce6eed fix(runtime/mpz): use size_t instead of unsigned long for Windows compatibility 2019-07-05 11:24:15 +02:00
Sebastian Ullrich
956a047d1e chore(library/compiler/extern_attribute): style 2019-02-14 14:07:05 -08:00
Leonardo de Moura
425a4b70d1 feat(library/init/data/int/basic): use extern attribute, and fix div/mod mess 
Now, int.div and int.mod behave like C++ `/` and `%` for int,
moreover, they satisfy

          (a/b)*b + (a%b) = a
 2019-02-12 11:41:46 -08:00
Leonardo de Moura
b2f3d3f456 chore(*): remove redundant code 2018-05-22 16:46:04 -07:00
Leonardo de Moura
dfc5adbd2a feat(runtime/lean_obj): add integer primitives 2018-05-17 17:47:22 -07:00
Leonardo de Moura
0556412f8d refactor(*): add runtime folder 
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
 2018-05-14 14:23:56 -07:00
Renamed from src/util/mpz.cpp (Browse further)