Christian Pehle
|
225fae9dc2
|
feat: add shiftLeft and shiftRight for UInt16 and UInt8
The same operations are implemented for UInt32, UInt64 and USize
already.
|
2021-01-14 15:30:35 +01:00 |
|
Sebastian Ullrich
|
0b146abeb1
|
chore: CI: don't schedule nightlies on forks
|
2021-01-14 15:04:45 +01:00 |
|
Sebastian Ullrich
|
5797ee4ab2
|
chore: CI: try to fix caching on Windows
|
2021-01-14 14:55:38 +01:00 |
|
Leonardo de Moura
|
5c91b395d6
|
chore: update stage0
|
2021-01-13 18:43:16 -08:00 |
|
Leonardo de Moura
|
e5b93783b0
|
test: TC issue repro
|
2021-01-13 18:41:01 -08:00 |
|
Leonardo de Moura
|
6e3792e995
|
chore: fix tests
|
2021-01-13 18:31:50 -08:00 |
|
Leonardo de Moura
|
bfc1a16c02
|
chore: adjust instance param order
|
2021-01-13 18:31:41 -08:00 |
|
Leonardo de Moura
|
74fbca5663
|
chore: update stage0
|
2021-01-13 16:34:31 -08:00 |
|
Leonardo de Moura
|
74a9331571
|
feat: use left-to-right resolution
|
2021-01-13 16:33:30 -08:00 |
|
Leonardo de Moura
|
8d9339a856
|
feat: improve error message position for termination check failures
|
2021-01-13 10:59:28 -08:00 |
|
Leonardo de Moura
|
f115c3919b
|
chore: update stage0
|
2021-01-13 10:36:38 -08:00 |
|
Leonardo de Moura
|
7a1fe0d235
|
chore: fix tests
|
2021-01-13 10:35:38 -08:00 |
|
Leonardo de Moura
|
8ddde1443c
|
test: sorry warning
|
2021-01-13 10:30:35 -08:00 |
|
Leonardo de Moura
|
e2773113a9
|
feat: add Float.neg and casts
|
2021-01-13 10:26:45 -08:00 |
|
Leonardo de Moura
|
b3703739af
|
chore: internal panic meesage
|
2021-01-13 10:26:25 -08:00 |
|
Leonardo de Moura
|
5e8dc62b94
|
chore: update stage0
|
2021-01-13 09:46:57 -08:00 |
|
Leonardo de Moura
|
b6bb31a131
|
feat: "compile" 'extern' axioms
|
2021-01-13 09:43:25 -08:00 |
|
Leonardo de Moura
|
f6e5b13591
|
feat: "implement" sorry using panic
|
2021-01-13 09:43:25 -08:00 |
|
Leonardo de Moura
|
3ca0aef098
|
feat: generate warning when sorry is used
|
2021-01-13 09:43:25 -08:00 |
|
Sebastian Ullrich
|
351285a2e8
|
fix: Nix: I still forget how to handle argument quoting in bash
|
2021-01-13 16:39:00 +01:00 |
|
Sebastian Ullrich
|
d1eeba3f74
|
feat: lean4-mode: allow setting lean4-rootdir after initialization
|
2021-01-13 16:39:00 +01:00 |
|
Sebastian Ullrich
|
a199f35330
|
fix: leanpkg: do not rely on PATH
|
2021-01-13 16:39:00 +01:00 |
|
Sebastian Ullrich
|
3a9658b91f
|
chore: obsolete comment
|
2021-01-13 16:39:00 +01:00 |
|
Leonardo de Moura
|
0c629b4a26
|
chore: fix tests
|
2021-01-12 17:19:38 -08:00 |
|
Leonardo de Moura
|
fdc0f906f4
|
feat: improve error message position for compiler errors
|
2021-01-12 17:10:11 -08:00 |
|
Sebastian Ullrich
|
1a8af48cca
|
doc: contribution guidelines & README update
|
2021-01-12 14:38:36 -08:00 |
|
Leonardo de Moura
|
9f7435b5be
|
chore: cleanup Message.toString
|
2021-01-12 09:57:46 -08:00 |
|
Sebastian Ullrich
|
74c2d1dca9
|
chore: remove io_state & abstract_type_context
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
4278480ea3
|
chore: remove io_state_stream
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
79abd5fec6
|
chore: remove C++ messages
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
298af4f749
|
chore: Nix: work around NixOS/nixpkgs#109033
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
a6c319a25c
|
chore: remove message_builder from time_task
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
1cb34604cd
|
chore: remove ios & message from tracing
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
b2e42a3ea6
|
chore: remove --json option
|
2021-01-12 09:51:14 -08:00 |
|
Sebastian Ullrich
|
7282470f24
|
fix: Message.toString: use same formatting as C++ code
|
2021-01-12 09:51:14 -08:00 |
|
Leonardo de Moura
|
e6a9f97c9b
|
chore: update stage0
|
2021-01-12 08:14:57 -08:00 |
|
Leonardo de Moura
|
42b5e780f5
|
chore: fix test
|
2021-01-12 08:14:16 -08:00 |
|
Leonardo de Moura
|
b6abf19656
|
fix: unfold abbreviations only
For example, we should not reduce types of the form `let x := ...; ...`
|
2021-01-12 08:11:04 -08:00 |
|
Leonardo de Moura
|
c1f3c724e1
|
fix: missing alternative
|
2021-01-12 07:44:31 -08:00 |
|
Leonardo de Moura
|
7160a010d1
|
chore: fix test
|
2021-01-12 06:58:35 -08:00 |
|
Leonardo de Moura
|
b5fdc5e364
|
fix: expand abbreviations at isClass?
|
2021-01-12 06:56:23 -08:00 |
|
Leonardo de Moura
|
1ebf69e163
|
fix: simple-match macro
|
2021-01-12 06:41:32 -08:00 |
|
Leonardo de Moura
|
9aaa52cf66
|
chore: update stage0
|
2021-01-11 16:41:29 -08:00 |
|
Leonardo de Moura
|
36008271ea
|
feat: ensure no unassigned metavariables in the declaration header when type is explicitly provided
|
2021-01-11 16:40:14 -08:00 |
|
Leonardo de Moura
|
3852ee16a0
|
chore: update stage0
|
2021-01-11 15:36:37 -08:00 |
|
Leonardo de Moura
|
8d0085ae31
|
feat: unification hints + type classes
|
2021-01-11 15:34:57 -08:00 |
|
Leonardo de Moura
|
ec7be1d801
|
feat: add processAssignment'
|
2021-01-11 15:22:10 -08:00 |
|
Leonardo de Moura
|
f0992c7022
|
chore: fix tests
|
2021-01-11 13:01:04 -08:00 |
|
Leonardo de Moura
|
e91df21e55
|
chore: update stage0
|
2021-01-11 12:55:39 -08:00 |
|
Leonardo de Moura
|
5b1b5bed0c
|
chore: naming convention
|
2021-01-11 12:52:51 -08:00 |
|