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

4634 commits

Author SHA1 Message Date
Leonardo de Moura
8649483b41 feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided 
closes #898
 2022-06-02 19:43:09 -07:00
Leonardo de Moura
484e510221 feat: do not use pp.inaccessibleNames = true at getInteractiveTermGoal 
See discussion at https://github.com/leanprover/vscode-lean4/issues/76

We also use `pp.inaccessibleNames = false` in error messages. In this
setting, an inaccessible name is displayed in the context only if the
target type depends on it.
 2022-06-02 16:22:43 -07:00
Leonardo de Moura
878ef3a281 feat: improve acyclic tactic 
closes #1182
 2022-06-02 15:25:14 -07:00
Sebastian Ullrich
1fff412b1f fix: regressions from previous commit 2022-06-02 19:04:47 +02:00
Sebastian Ullrich
ddfbf6bf9b fix: show namespace when hovering over declaration name 2022-06-02 18:17:21 +02:00
Leonardo de Moura
32db316166 fix: enumeration type noConfusion was not registered 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20function.20expected.20.2EnoConfusion/near/284634050
 2022-06-01 17:58:46 -07:00
Gabriel Ebner
9a273b85a3 fix: no sorry-warning for missing match cases 2022-06-01 07:41:52 -07:00
Leonardo de Moura
9102f8cb13 fix: generate sorry warning only if there are no error messages 
see #1163
 2022-06-01 06:32:05 -07:00
Leonardo de Moura
64c36fffda feat: generate warning message if declaration has a non-synthetic sorry 
closes #1163
 2022-05-31 18:00:48 -07:00
Leonardo de Moura
0631c90794 feat: implement MonadLog at CoreM 2022-05-31 17:40:55 -07:00
Leonardo de Moura
caa79ca04f refactor: move MonadLog 2022-05-31 16:50:48 -07:00
Leonardo de Moura
be69d04af4 feat: add Declaration.hasSorry 2022-05-31 16:39:37 -07:00
Leonardo de Moura
5f7cc78f17 fix: remove unnecessary let-expressions when computing the motive 
fixes #1155
 2022-05-31 07:14:56 -07:00
Leonardo de Moura
704242f865 feat: zetaReduce should expand nested let-expressions too 2022-05-31 07:01:52 -07:00
Leonardo de Moura
d8aab852e8 feat: add usedLetOnly parameter to Meta.transform 2022-05-31 07:00:53 -07:00
Leonardo de Moura
e997cd94c6 chore: style 2022-05-31 06:04:48 -07:00
larsk21
a741540400 fix: relax InfoTree.visitM when visiting holes 2022-05-31 13:14:24 +02:00
Wojciech Nawrocki
115c564b18 feat: go to head constant in applications 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
737e872ee0 feat: set tagAppFns in explicit exprToInteractive 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
9c9407e722 feat: propagate tagAppFns in delaborator 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
cd47c30e47 chore: review fixes 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
8c67afae2f feat: generalize getGoToLocation RPC 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
8c5cebfb11 chore: default optional LSP fields 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
aef8d32d0b feat: add RPC call to retrieve defn/decl/type defn 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
9c058a5798 chore: remove some unnecessary partial 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
e555490ee2 feat: store subexpression positions 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
25a8646a5f feat: add showDocument client capability 2022-05-31 00:07:56 +02:00
ammkrn
102e957bb5 feat: support proofs in deriving DecidableEq 
The derive handler for `DecidableEq` does not currently support proofs
in constructor arguments/structure fields. For example, deriving
`DecidableEq` for `Fin n` will fail, because of the field `isLt`. This
change checks whether the elements being tested are proofs, and if so,
changes the equality proof to just `rfl`.
 2022-05-30 07:36:30 -07:00
Leonardo de Moura
9818de078b fix: fixes #1168 2022-05-30 07:24:23 -07:00
Leonardo de Moura
fb45eb4964 fix: universe polymorphic enumeration types 
Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20number.20of.20universe.20levels.20parameters/near/284283021
 2022-05-30 06:43:46 -07:00
Leonardo de Moura
b0efae4823 chore: style 2022-05-30 06:43:46 -07:00
Sebastian Ullrich
ef9976ccda fix: do not discard macro exceptions in expandMacro? 2022-05-30 13:28:42 +02:00
Sebastian Ullrich
d3cf60e86a chore: further refine goal state heuristics 2022-05-30 13:27:56 +02:00
Sebastian Ullrich
b31690b1d7 fix: go to definition/goal state at end of syntax 2022-05-30 11:16:25 +02:00
Leonardo de Moura
40fc64480a feat: add tactic subst_vars 2022-05-28 16:19:34 -07:00
Leonardo de Moura
2c5bafcbd8 fix: dead variables at match equation hypotheses 
This commit addresses an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structural.20Recursion.20Problem/near/284238723
 2022-05-28 16:09:35 -07:00
Leonardo de Moura
e26f86dd45 fix: improve simpH?, remove unnecessary hypotheses 2022-05-28 15:30:01 -07:00
Leonardo de Moura
fbd8224b4d fix: allow recursive occurrences in binder types at WF/PackDomain.lean 
fixes #1171
 2022-05-27 11:23:51 -07:00
Leonardo de Moura
3be437cad3 fix: make sure register_simp_attr declares an simp-like attribute parser for user simp attributes 
closes #1164
 2022-05-26 19:49:33 -07:00
Leonardo de Moura
7d8f8c0fbe chore: style 2022-05-26 15:18:07 -07:00
Leonardo de Moura
25126cd057 fix: autoParam is structure fields lost in multiple inheritance 
closes #1158
 2022-05-26 14:35:47 -07:00
Leonardo de Moura
f48b822532 feat: add field for storing autoParam information at StructureFieldInfo 
We need this information when copying fields from parent structures.
We don't use hacks such as traversing the parent constructor type.
 2022-05-26 14:21:03 -07:00
Leonardo de Moura
dcb974a1cf chore: remove unused parameter 2022-05-26 14:20:51 -07:00
Leonardo de Moura
fc606f3ab5 fix: closes #1156 2022-05-26 12:51:28 -07:00
Leonardo de Moura
988697b431 fix: fixes #1169 2022-05-26 07:05:32 -07:00
Leonardo de Moura
1d14637680 fix: missing withMVarContext 2022-05-26 06:18:14 -07:00
Leonardo de Moura
fad21a4cda chore: remove leftovers 2022-05-25 20:38:20 -07:00
Leonardo de Moura
dca8a8ed98 fix: match or-pattern 
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Probably.20a.20bug/near/283779934
 2022-05-25 20:05:46 -07:00
Leonardo de Moura
bef1cd4872 fix: make structure instance notation (e.g., { a, b }) works in patterns after we define the Set notation in Mathlib 2022-05-25 19:14:22 -07:00
Leonardo de Moura
a26827f58b chore: remove Context.main 2022-05-25 11:58:33 -07:00