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

26562 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
5f0def2edf chore: update stage0 2021-12-13 10:39:19 -08:00
Leonardo de Moura
55db56f80d feat: add noncomputable section parser 2021-12-13 10:35:16 -08:00
Sebastian Ullrich
0ade9ee39b fix: make IO.Process.Child.wait fallible 2021-12-13 15:12:48 +01:00
Leonardo de Moura
3a6cc77424 chore: update lake 2021-12-12 08:29:30 -08:00
Leonardo de Moura
133c58aba2 chore: update stage0 2021-12-12 08:17:30 -08:00
Leonardo de Moura
bf3b0c53ad chore: add helper parser 2021-12-12 08:16:42 -08:00
Leonardo de Moura
b2e065a3ba chore: avoid where structure instance notation 
This is a workaround to avoid staging issues.
 2021-12-12 07:59:38 -08:00
Leonardo de Moura
b6ef65d8fd fix: where structure instance parser 
closes #753
 2021-12-12 07:52:52 -08:00
Leonardo de Moura
a3361e7d86 fix: missing universe assignments made during TC resolution 
closes #796
 2021-12-12 07:07:13 -08:00
Sebastian Ullrich
a91b861919 Revert "chore: CI: propagate prepare-*.sh errors" 
This reverts commit 198d3103cd.
 2021-12-11 17:37:12 +01:00
Sebastian Ullrich
198d3103cd chore: CI: propagate prepare-*.sh errors 2021-12-11 09:51:27 +01:00
Sebastian Ullrich
ed3dad9313 fix: bundling on Linux 2021-12-11 09:10:06 +01:00
tydeu
d785652792 chore: update Lake 2021-12-10 16:38:31 -08:00
Leonardo de Moura
d5f1a5d1d1 fix: in-word completion 
closes #857
 2021-12-10 15:48:35 -08:00
Sebastian Ullrich
fddbc3c09e fix: empty option completion 2021-12-10 14:19:19 -08:00
Sebastian Ullrich
a4633d30e2 fix: option completion after trailing . 2021-12-10 14:19:19 -08:00
Sebastian Ullrich
74dba7c64e fix: do not hide trace messages on partial syntax 2021-12-10 14:19:19 -08:00
Sebastian Ullrich
ce2e733f17 fix: make option completion work in presence of value 2021-12-10 14:19:19 -08:00
Leonardo de Moura
1003840376 chore: update lake 2021-12-10 13:20:27 -08:00
Leonardo de Moura
63decd445c chore: fix test 2021-12-10 13:13:03 -08:00
Leonardo de Moura
68bd55af32 chore: fix codebase 2021-12-10 13:12:09 -08:00
Leonardo de Moura
d9d44baabe chore: update stage0 2021-12-10 12:56:00 -08:00
Leonardo de Moura
483f32edd8 feat: in pure code, do use assume Id monad at do notation 
This feature produced counterintuitive behavior and confused users.
See discussion at #770.

As pointed out by @tydeu, it is not too much work to write `Id.run <|`
before the `do` when we want to use the `do` notation in pure code.

closes #770
 2021-12-10 12:55:14 -08:00
Leonardo de Moura
96e0e1db98 fix: nontermination at simp [OfNat.ofNat] 
closes #788
 2021-12-10 12:29:33 -08:00
Leonardo de Moura
47c2d335d4 fix: completion for aliases 
closes #863
 2021-12-10 12:14:11 -08:00
Leonardo de Moura
84f374702d feat: add fields isInstance and isType to InteractiveHypothesis 
see https://github.com/leanprover/vscode-lean4/issues/76
 2021-12-10 09:08:55 -08:00
Sebastian Ullrich
5796bb835c fix: Nix: shell.nix on macOS 2021-12-10 16:13:45 +01:00
Joscha
d19cfede02 fix: implement suggestions 2021-12-10 15:25:43 +01:00
Joscha
e4406f1785 fix: find references to function parameters in function body 
With #861, the server can now connect the occurrences of parameters in the
function definition and in the function body to each other.
 2021-12-10 15:25:43 +01:00
Joscha
12ee541622 fix: reference fields in constructor correctly 2021-12-10 15:25:43 +01:00
Joscha
11ba6dc216 test: add simple "find references" test 2021-12-10 15:25:43 +01:00
Joscha
2823cbc87b feat: implement single-file "find references" in LSP server 2021-12-10 15:25:43 +01:00
Leonardo de Moura
e64cfbb9b2 test: well-founded recursion example 
see #860
 2021-12-09 14:32:06 -08:00
Leonardo de Moura
45f5909dd0 chore: register Elab.resume trace class 2021-12-09 13:37:39 -08:00
Sebastian Ullrich
77aed3a0b1 fix: add binder info nodes for parameter copies in body 2021-12-09 18:12:51 +01:00
Leonardo de Moura
da33f498f5 feat: show argument name at "don't know how to synthesize placeholder" error messages 2021-12-09 06:48:06 -08:00
Leonardo de Moura
ff90459fd2 feat: add Lean.Elab.Term.getMVarErrorInfo? 2021-12-09 06:48:06 -08:00
Leonardo de Moura
914f181641 feat: add ForIn instance for MVarIdMap 2021-12-09 06:48:06 -08:00
Sebastian Ullrich
a91e5d69f3 chore: lean4-mode: save buffer in lean4-diff-test-file 2021-12-09 15:45:45 +01:00
Michael Burge
6d57299396 chore: set Nix flake's defaultPackage to lean-all for interactive use 
Allows Nix flake to run tutorial and other simple examples out-of-the-box.

Closes #858
 2021-12-09 12:06:25 +01:00
Sebastian Ullrich
265c18accd doc: faq: bullet points look weird and are not anchors 2021-12-09 11:53:25 +01:00
Leonardo de Moura
d3713e8952 chore: update stage0 2021-12-07 16:44:26 -08:00
Leonardo de Moura
41040a81de fix: auxiliary matcher definitions should be treated as abbreviations 
The motivation is to prevent performance problems such as the one
described at issue #854.

Fixes #854 after a update stage0
 2021-12-07 16:43:20 -08:00
Leonardo de Moura
b0fe1e5d10 feat: add Tomas Skrivan's TC resolution improvement 
This commit implements the TC resolution improvement suggested by
Tomas at #815.

Closes #815.
 2021-12-06 17:46:11 -08:00
Wojciech Nawrocki
c97487fd65 feat: add blackboard bold characters 2021-12-06 17:45:44 -08:00
Wojciech Nawrocki
c57a664127
feat: lean4-mode: add missing mathematical scripts 2021-12-06 23:16:22 +01:00
Leonardo de Moura
7b6732a137 refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files 
We use the export/extern idiom to define `isLevelDefEqAux`, and then
define the `isDefEq` user facing functions at `Meta/Basic.lean`.
 2021-12-06 09:57:00 -08:00
Sebastian Ullrich
f0fa6dcbc5 refactor: remove unnecessary Lean.Elab.Term imports 2021-12-06 09:28:56 -08:00
Leonardo de Moura
7de749a23c refactor: move setElabConfig to Elab directory 
see #849
 2021-12-06 08:12:59 -08:00
Severen Redwood
af944e69c0 doc: fix typo in documentation for sorry tactic 2021-12-06 17:12:31 +01:00