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

5505 commits

Author SHA1 Message Date
Leonardo de Moura
3dbd2b728b feat: add Array.getMax? 2020-09-04 10:40:34 -07:00
Leonardo de Moura
555a3f0dcf feat: new and improved mkAuxDefinition 2020-09-03 17:37:06 -07:00
Leonardo de Moura
f34fd3e6b4 refactor: move Closure.lean to Meta 
We will need to improve the support for let-decls. We will use
the new `trackZeta`.
 2020-09-03 11:54:08 -07:00
Leonardo de Moura
ad774ae397 feat: support for tracking which let-decls have been zeta expanded 2020-09-03 11:32:46 -07:00
Leonardo de Moura
f2a6562eed feat: validate 'let rec' types 2020-09-02 17:02:40 -07:00
Leonardo de Moura
8aa5409bac feat: elaborate 'let rec' 
Remark: the actual lift is going to be performed at `MutualDef.lean`.
 2020-09-02 17:02:35 -07:00
Leonardo de Moura
93bc39f897 chore: parameters do not need to match in mutually recursive definitions 2020-09-02 10:30:35 -07:00
Leonardo de Moura
907a202961 feat: expand in command macro 2020-09-02 10:04:58 -07:00
Leonardo de Moura
988bb09aaf feat: new inductive command syntax 
cc @Kha
 2020-09-02 09:41:52 -07:00
Leonardo de Moura
c5cd5f2e5b feat: check kinds 2020-09-01 17:20:06 -07:00
Leonardo de Moura
d74551b19e feat: elaborate header of mutually recursive definitions 2020-09-01 16:13:04 -07:00
Leonardo de Moura
095e07d52d chore: letrec => let rec 
cc @Kha
 2020-09-01 13:27:41 -07:00
Leonardo de Moura
5e5b75af61 chore: remove withDeclId 2020-09-01 13:04:08 -07:00
Leonardo de Moura
d7e99c76c3 feat: mutual + namespace macro 2020-09-01 12:25:29 -07:00
Wojciech Nawrocki
f3d640a7cf feat: report parser errors in server 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
7b971c6cc5 fix: server test 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
23feb04d60 chore: clean up LSP code style and add more definitions from the spec 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
098c7af1b6 feat: server tests 2020-08-31 06:50:01 -07:00
Sebastian Ullrich
75b2dc1baf refactor: simplify ppModule using new module parser 2020-08-31 15:44:58 +02:00
Sebastian Ullrich
6b1df15518 chore: ignore test output files 2020-08-31 11:09:27 +02:00
Sebastian Ullrich
c88784ef9d refactor: consistent io_result_mk* naming 
/cc @leodemoura
 2020-08-31 11:08:57 +02:00
Leonardo de Moura
2f4340f63c feat: refine refine tactic 
Now `refine stx` reports an error when there are natural unassigned
metavariables after we elaborate syntax `stx`. The idea is that only
synthetic holes `?<hole-name>` become new goals.
The tactic `refine! stx` implements the Lean3 behavior.
 2020-08-30 16:14:38 -07:00
Sebastian Ullrich
8ed4d1d7e4 test: test process exit code 2020-08-30 14:28:56 -07:00
Sebastian Ullrich
8b79e0f28c test: robustly fix test on Windows 2020-08-30 14:28:56 -07:00
Sebastian Ullrich
3546c8c355 chore: always show test diff 2020-08-30 14:28:56 -07:00
Sebastian Ullrich
cc909e20e1 fix: handle SIGPIPE 2020-08-30 14:28:56 -07:00
Sebastian Ullrich
9f40e46043 feat: basic process API 2020-08-30 14:28:56 -07:00
Leonardo de Moura
6f0e9452b2 chore: remove begin ... end syntax 
We should use `by { ... }` from now on.

cc @Kha
 2020-08-30 14:15:33 -07:00
Leonardo de Moura
b74741b741 chore: "begin ... end" ==> "by { ... }" 
cc @Kha
 2020-08-30 14:01:27 -07:00
Leonardo de Moura
052e830db7 feat: add have, show, let, let!, and suffices tactic macros 
They are all simple macros based on: `refine` + syntheticHoles
 2020-08-30 08:26:15 -07:00
Leonardo de Moura
825d9643cd feat: allow structure instances as fun binder without () 
The issue is that `{ x := ... }` was being parsed as an implicit
binder, and we were getting an error at `:=`.
 2020-08-30 07:35:41 -07:00
Leonardo de Moura
2eb330e36a feat: improve clear tactic 2020-08-29 20:19:33 -07:00
Leonardo de Moura
9e075e39a5 feat: eval new intro "macro" 
It is as powerful as the new `fun` term
 2020-08-29 17:09:21 -07:00
Leonardo de Moura
3d3238c7fe fix: typo at introNCoreAux 2020-08-29 17:00:59 -07:00
Leonardo de Moura
52c86e918d fix: match 2020-08-29 16:38:50 -07:00
Sebastian Ullrich
9c6ff0baac chore: certainly this one is the right fix 2020-08-29 12:56:37 +02:00
Sebastian Ullrich
0b727a6d78 chore: fix stdlib benchmark once more... 2020-08-29 10:40:21 +02:00
Leonardo de Moura
99f3296828 refactor: simplify Util/Trace.lean 2020-08-28 17:36:44 -07:00
Leonardo de Moura
e0d39e6a7d feat: use whnf at subst 2020-08-28 15:56:28 -07:00
Leonardo de Moura
2287c7e7b3 feat: elaborate #print axioms command 2020-08-28 13:08:42 -07:00
Leonardo de Moura
50470c328f test: nativeRefl! abuse example 2020-08-28 12:09:25 -07:00
Sebastian Ullrich
110ae4b571 feat: replace OS-specific stream redirection with pure-Lean Stream redirection 
This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.
 2020-08-28 10:04:32 -07:00
Sebastian Ullrich
efa119bc94 feat: make std streams Streams 2020-08-28 10:04:32 -07:00
Sebastian Ullrich
dbebff3a2d feat: ByteArray.copySlice 2020-08-28 10:04:32 -07:00
Sebastian Ullrich
1b0ffbb74d feat: make std IO streams settable 
Co-authored-by: Simon Hudon <simon.hudon@gmail.com>
 2020-08-28 10:04:32 -07:00
Leonardo de Moura
54f95421c8 test: Lean2 obtain is just a macro 2020-08-28 09:37:29 -07:00
Leonardo de Moura
62177069fd fix: induction tactic 2020-08-28 09:18:22 -07:00
Leonardo de Moura
0b7a7f7b90 feat: better support for _ in match tactic 2020-08-27 18:18:49 -07:00
Leonardo de Moura
76bda91ff8 feat: add evalMatch for tactics 2020-08-27 18:05:06 -07:00
Leonardo de Moura
6f1975aef5 feat: report errors for unassigned metavariables 
We were not reporting unassigned metavariables due to
1- `_`
2- Named holes (e.g., `?x`)
3- Implicit arguments
 2020-08-27 15:03:41 -07:00