Leonardo de Moura
|
42773941ed
|
chore: fix test
|
2021-10-02 17:00:07 -07:00 |
|
Leonardo de Moura
|
740aab923d
|
chore: update stage0
|
2021-10-02 16:57:40 -07:00 |
|
Leonardo de Moura
|
1e44902243
|
fix: add withFreshMacroScope at expandMacroImpl?
|
2021-10-02 16:57:25 -07:00 |
|
Leonardo de Moura
|
deb77b62df
|
chore: update stage0
|
2021-10-02 16:28:47 -07:00 |
|
Leonardo de Moura
|
15347272c7
|
feat: elaborate wait_* notation
We can use to define `if-then-else` using macros
|
2021-10-02 16:27:22 -07:00 |
|
Leonardo de Moura
|
b510bb305d
|
feat: elaborate let_mvar%
|
2021-10-02 16:12:50 -07:00 |
|
Leonardo de Moura
|
59d7b00557
|
feat: add mapping from mvar user name to MVarId
|
2021-10-02 15:26:44 -07:00 |
|
Leonardo de Moura
|
98f1ab7816
|
chore: update stage0
|
2021-10-02 15:12:51 -07:00 |
|
Leonardo de Moura
|
c6dfecb7aa
|
feat: helper notation for controlling elaboration order
|
2021-10-02 15:10:27 -07:00 |
|
Leonardo de Moura
|
acd21052c0
|
chore: remove old notation
|
2021-10-02 15:06:40 -07:00 |
|
Leonardo de Moura
|
74329f6713
|
chore: update stage0
|
2021-10-02 14:56:09 -07:00 |
|
Leonardo de Moura
|
9337498c5b
|
chore: keywords should be snake_case
|
2021-10-02 14:54:48 -07:00 |
|
Leonardo de Moura
|
b7281e9fe2
|
fix: instruct pretty printer to add a line break after each calc step
It should fix https://github.com/leanprover/mathport/issues/26
|
2021-10-02 11:38:10 -07:00 |
|
Daniel Fabian
|
e1f591ba61
|
test: do no use unit in ac_expr.lean.
It is not necessary to define a unit element for the proof to go through.
|
2021-10-02 11:11:08 -07:00 |
|
Siddharth
|
4b1b76ae51
|
doc: add metaprogramming docs of Dyck grammar parsing.
* LEAN4 -> Lean 4; directive -> command
* directive -> command everywhere
|
2021-10-02 11:08:26 -07:00 |
|
Wojciech Nawrocki
|
f454850c70
|
fix: actually specify opts-per-pos
|
2021-10-02 09:55:55 +02:00 |
|
Sebastian Ullrich
|
af12c91b0a
|
fix: rpath rewrite leanc as well
|
2021-10-01 10:06:50 +02:00 |
|
Leonardo de Moura
|
01ca9a06c1
|
chore: update stage0
|
2021-09-30 22:38:31 -07:00 |
|
Leonardo de Moura
|
dba358067a
|
chore: remove workaround
|
2021-09-30 22:37:20 -07:00 |
|
Leonardo de Moura
|
3833363be8
|
chore: update stage0
|
2021-09-30 22:35:40 -07:00 |
|
Leonardo de Moura
|
b99f1c698b
|
feat: use if-then-else notation at Do.lean
Otherwise, the `if` in the `Do` notation will not benefit from the
improved elaborator.
|
2021-09-30 22:34:36 -07:00 |
|
Leonardo de Moura
|
9d9f41c27a
|
chore: update stage0
|
2021-09-30 22:24:22 -07:00 |
|
Leonardo de Moura
|
2546a2cf7e
|
test: add test for if-then-else issue
The issue was reported here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Required.20type.20annotation.20using.20Array
|
2021-09-30 22:23:22 -07:00 |
|
Leonardo de Moura
|
eedf5b245f
|
feat: use let_tmp at new if-then-else elaborator
|
2021-09-30 22:22:14 -07:00 |
|
Leonardo de Moura
|
35d9590b7b
|
chore: rename let_tmp elaborator
|
2021-09-30 22:20:32 -07:00 |
|
Leonardo de Moura
|
94dc1ee38f
|
chore: update stage0
|
2021-09-30 22:19:42 -07:00 |
|
Leonardo de Moura
|
2bc24ff619
|
chore: let_zeta => let_tmp
|
2021-09-30 22:19:06 -07:00 |
|
Leonardo de Moura
|
035251d08a
|
feat: elaborate let_zeta
|
2021-09-30 22:18:47 -07:00 |
|
Leonardo de Moura
|
cfa9d5a0b6
|
chore: update stage0
|
2021-09-30 22:09:45 -07:00 |
|
Leonardo de Moura
|
b83facc738
|
feat: add let_zeta auxiliary parser
|
2021-09-30 22:08:11 -07:00 |
|
Leonardo de Moura
|
cc920dd26b
|
feat: new if-then-else elaborator that waits for condition type to be known
|
2021-09-30 22:07:32 -07:00 |
|
Leonardo de Moura
|
7c0993ae12
|
chore: add pp annotations to if parser
|
2021-09-30 20:40:02 -07:00 |
|
Leonardo de Moura
|
2aa190ec6a
|
chore: update stage0
|
2021-09-30 20:34:56 -07:00 |
|
Leonardo de Moura
|
88c73f1daa
|
chore: remove old if-then-else parser and elaborator
|
2021-09-30 20:33:58 -07:00 |
|
Leonardo de Moura
|
a7fc07a8b4
|
chore: update stage0
|
2021-09-30 20:33:15 -07:00 |
|
Leonardo de Moura
|
7ea23a0f37
|
chore: reduce priority of old if-then-else parser
|
2021-09-30 20:31:54 -07:00 |
|
Leonardo de Moura
|
ef4becfedb
|
chore: update stage0
|
2021-09-30 20:31:18 -07:00 |
|
Leonardo de Moura
|
a5502e652c
|
chore: activate builtin if-then-else elaborator
|
2021-09-30 20:29:49 -07:00 |
|
Leonardo de Moura
|
bc578f17ad
|
chore: update stage0
|
2021-09-30 19:34:21 -07:00 |
|
Leonardo de Moura
|
698760c5eb
|
refactor: add if-then-else builtin parser
|
2021-09-30 19:33:41 -07:00 |
|
Leonardo de Moura
|
58743b983e
|
chore: update stage0
|
2021-09-30 12:50:40 -07:00 |
|
Leonardo de Moura
|
32b6172449
|
chore: update stage0
|
2021-09-30 12:48:50 -07:00 |
|
Leonardo de Moura
|
28d81ee456
|
fix: do not extract closed terms containing constants being defined
It may produce crashes during initialization.
|
2021-09-30 12:46:38 -07:00 |
|
Leonardo de Moura
|
837677cb4c
|
test: doc string
|
2021-09-30 11:27:09 -07:00 |
|
Leonardo de Moura
|
db5df69db4
|
fix: bounds check
fixes #704
|
2021-09-30 07:55:10 -07:00 |
|
Sebastian Ullrich
|
9569d7997c
|
chore: update Nix
|
2021-09-30 13:34:26 +02:00 |
|
Sebastian Ullrich
|
ee73ad9f23
|
chore: update mdBook fork
|
2021-09-30 13:02:39 +02:00 |
|
Sebastian Ullrich
|
f9ab429f75
|
fix: Nix build
|
2021-09-30 10:24:45 +02:00 |
|
Leonardo de Moura
|
ff38774b95
|
test: printDecls
|
2021-09-29 17:44:21 -07:00 |
|
Leonardo de Moura
|
09d0c93589
|
feat: declare functions in mutual block using auxiliary fuction defined using WF
|
2021-09-29 11:24:52 -07:00 |
|