Sebastian Ullrich
|
70f99ab655
|
chore: placate GCC
|
2021-09-23 16:31:41 +02:00 |
|
Sebastian Ullrich
|
6eca75ddbd
|
fix: include exported declarations in defining file
|
2021-09-20 18:41:46 +02:00 |
|
Leonardo de Moura
|
ca6941ab39
|
chore: rename lean_mpz_value
|
2021-09-11 17:00:47 -07:00 |
|
Leonardo de Moura
|
f9bc4b9b3a
|
feat: add missing APIs
|
2021-09-11 15:39:11 -07:00 |
|
Leonardo de Moura
|
075ba63a8b
|
feat: add LEAN_ABORT_ON_PANIC
|
2021-09-09 04:49:16 -07:00 |
|
Leonardo de Moura
|
c8406a301d
|
chore: reduce src/include/lean
|
2021-09-07 08:24:54 -07:00 |
|
Leonardo de Moura
|
6ced2cdece
|
refactor: move lean_name_eq to runtime, add lean_name_hash in C
|
2021-08-16 16:13:55 -07:00 |
|
Leonardo de Moura
|
14b611af96
|
refactor: move buffer.h and *_ref.h files to runtime
|
2021-08-16 15:39:38 -07:00 |
|
Leonardo de Moura
|
10122ba38b
|
chore: try to fix compilation error at CI
|
2021-07-20 10:42:28 -07:00 |
|
Leonardo de Moura
|
286136b3c7
|
fix: missing std::
|
2021-07-20 10:42:28 -07:00 |
|
Leonardo de Moura
|
c59e72a77b
|
chore: cleaner lean_dec_ref, inline persistent object case
|
2021-07-20 10:42:28 -07:00 |
|
Leonardo de Moura
|
da66610fda
|
chore: cleanup
|
2021-07-20 10:42:28 -07:00 |
|
Leonardo de Moura
|
489b28085f
|
feat: simpler and faster RC
|
2021-07-20 10:42:28 -07:00 |
|
Leonardo de Moura
|
d0358810a7
|
feat: add lean_set_panic_messages
|
2021-06-29 14:30:56 -07:00 |
|
Leonardo de Moura
|
5ac2e14173
|
chore: add Hashable that uses UInt64
|
2021-06-02 07:47:41 -07:00 |
|
Leonardo de Moura
|
c566ad97a4
|
chore: prepare to use UInt64 hash codes
|
2021-06-02 06:51:18 -07:00 |
|
Sebastian Ullrich
|
7b128b308b
|
fix: leak in lean_mk_array
|
2021-05-07 18:20:32 +02:00 |
|
Leonardo de Moura
|
104b51471c
|
chore: fix warning
|
2021-04-22 20:38:57 -07:00 |
|
Leonardo de Moura
|
df665bc219
|
chore: remove leftover
|
2021-04-22 20:34:52 -07:00 |
|
Sebastian Ullrich
|
8895ed47e5
|
refactor: clean up Thunk
Fixes a bug in the native implementation of `Thunk.bind` by deleting it
|
2021-04-22 20:29:08 -07:00 |
|
Leonardo de Moura
|
393adadf9a
|
chore: leftovers
|
2021-04-07 10:26:05 -07:00 |
|
Leonardo de Moura
|
9901898258
|
feat: add Nat.gcd
This commit also fix some theorem names to new naming convention.
|
2021-03-07 18:47:02 -08:00 |
|
Leonardo de Moura
|
709eaf6873
|
chore: use lean_internal_panic
|
2021-03-04 15:46:33 -08:00 |
|
Joe Hendrix
|
9bd60c7519
|
feat: Nat/Fin/UInt instances of bitwise classes
|
2021-03-04 15:42:43 -08:00 |
|
Leonardo de Moura
|
130a087ecf
|
feat: Lean 3 french single quote notation
|
2021-03-04 09:43:59 -08:00 |
|
Leonardo de Moura
|
bbed4aed50
|
chore: remove old code
|
2021-03-04 07:54:21 -08:00 |
|
Leonardo de Moura
|
51200c916e
|
chore: make explicit user and internal panics
|
2021-03-04 07:37:33 -08:00 |
|
Leonardo de Moura
|
09ad6cc50a
|
fix: fixes #306 fixes #307
|
2021-02-06 12:31:51 -08:00 |
|
Leonardo de Moura
|
10a10b38d8
|
fix: fixes #303
|
2021-02-05 07:53:18 -08:00 |
|
Leonardo de Moura
|
22a7a9e313
|
fix: missing lean_inc
|
2021-01-31 12:07:24 -08:00 |
|
Leonardo de Moura
|
f9ebfb466f
|
fix: missing lean_inc
|
2021-01-31 11:18:57 -08:00 |
|
Leonardo de Moura
|
36e70e9a08
|
fix: Int.mod implementation in the runtime
|
2021-01-31 08:50:06 -08:00 |
|
Leonardo de Moura
|
3fa1f355eb
|
fix: mod implementation
|
2021-01-31 08:19:32 -08:00 |
|
Leonardo de Moura
|
b3703739af
|
chore: internal panic meesage
|
2021-01-13 10:26:25 -08:00 |
|
Leonardo de Moura
|
f6e5b13591
|
feat: "implement" sorry using panic
|
2021-01-13 09:43:25 -08:00 |
|
Sebastian Ullrich
|
5aab1cadc0
|
chore: remove debug print
|
2021-01-02 22:00:30 +01:00 |
|
Sebastian Ullrich
|
4a262fbc5b
|
fix: remove auto-cancellation of IO tasks
Chained tasks were never auto-canceled, so let's be explicit everywhere
|
2020-12-30 17:03:09 +01:00 |
|
Sebastian Ullrich
|
91dac6ccff
|
fix: race condition in Task.bind
|
2020-12-30 17:01:05 +01:00 |
|
Leonardo de Moura
|
c71eebde8c
|
chore: remove util/buffer.h dependency from runtime
|
2020-12-14 18:07:28 -08:00 |
|
Leonardo de Moura
|
bbafaf8805
|
fix: Array.mk and Array.data externs
|
2020-12-13 11:10:01 -08:00 |
|
Leonardo de Moura
|
6a41d04827
|
fix: missing panics
|
2020-12-08 10:36:53 -08:00 |
|
Leonardo de Moura
|
b95c4788c1
|
refactor: OfDecimal ==> OfScientific
`decimalLit` ==> `scientificLit`
|
2020-12-03 08:08:19 -08:00 |
|
Leonardo de Moura
|
d1f4d4f57e
|
feat: scientific notation
|
2020-12-03 07:49:20 -08:00 |
|
Leonardo de Moura
|
962cffbaaa
|
feat: add lean_float_of_decimal using GMP
|
2020-12-03 06:15:18 -08:00 |
|
Sebastian Ullrich
|
a22d234e93
|
fix: Thunk.get: mark result as MT before storing it in the task object
|
2020-11-29 18:59:39 +01:00 |
|
Sebastian Ullrich
|
3e09184a39
|
fix: String.mk, String.toList
|
2020-10-16 09:42:59 +02:00 |
|
Sebastian Ullrich
|
8b62665788
|
chore: print dbg* output to stderr
|
2020-10-12 10:01:29 +02:00 |
|
Sebastian Ullrich
|
c83529810d
|
fix: avoid deadlock on freeing task-carrying task
|
2020-10-11 17:43:28 +02:00 |
|
Sebastian Ullrich
|
ab6b6ac3ba
|
feat: add dedicated task priority
|
2020-09-29 08:01:10 -07:00 |
|
Sebastian Ullrich
|
562c7ed5ce
|
feat: expose task priorities
|
2020-09-29 08:01:10 -07:00 |
|