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

4381 commits

Author SHA1 Message Date
Leonardo de Moura
fa9b0f6c7e feat: remove space before propositions with inaccessible names 2022-04-07 07:54:50 -07:00
Leonardo de Moura
911ed750ff doc: document ▸ 2022-04-06 16:30:02 -07:00
Leonardo de Moura
005f964749 feat: save info at renameInaccessibles 
We now have info variables introduced by the `next` and `case` tactics
 2022-04-06 16:16:20 -07:00
Leonardo de Moura
847f5b21a6 feat: save info for cases and induction alt vars 2022-04-06 15:53:58 -07:00
Leonardo de Moura
0bfcf434ac fix: jump to definition inside of a mutually inductive declaration 2022-04-06 14:43:30 -07:00
Leonardo de Moura
1107705525 fix: jump to definition inside recursive definitions was not working on VS Code 
Remark: it was working on Emacs.
 2022-04-06 14:27:49 -07:00
Leonardo de Moura
574927ab0d fix: jump to definition for recursive declarations 2022-04-06 13:01:16 -07:00
Leonardo de Moura
d380808930 fix: generalize if target is a let-declaration 2022-04-06 11:08:41 -07:00
Sebastian Ullrich
24697026e8 feat: always accept antiquotations, simplify quotDepth code 2022-04-06 19:43:07 +02:00
Sebastian Ullrich
e10e664cc1 chore: typos 2022-04-06 10:21:53 +02:00
Sebastian Ullrich
3cf2afa42e refactor: clean up parsers using withAnonymousAntiquot := false 2022-04-06 10:21:53 +02:00
Sebastian Ullrich
ffee6676ef feat: allow adjusting anonymous antiquot generation at leading_parser 2022-04-06 10:21:53 +02:00
Sebastian Ullrich
99464c352e chore: remove restriction on leading/trailing_parser macros 
I don't think we quote any parsers right now
 2022-04-06 10:21:53 +02:00
Leonardo de Moura
058aea8922 fix: withSaveInfoContext at Inductive.lean 
It was in the context of `withInductiveLocalDecls`. This introduced
unnecessary `_root_` in the info view and hover information.

For example, when hovering over
```lean
inductive Ty where
  | int
  | bool
  | fn (a r : Ty)
```
We would get `Ty.int : _root_.Ty` when hovering over the `int`.
 2022-04-05 20:58:06 -07:00
Leonardo de Moura
7c5575631a feat: remove _tmp_ind_univ_param elaboration hack 
The new approach produces better type information in the "info view" when
hovering over inductive declarations.
 2022-04-05 20:51:15 -07:00
Leonardo de Moura
27e07d1b25 fix: remove auxiliary discriminants before elaborating patterns 2022-04-05 19:37:56 -07:00
Leonardo de Moura
eae4b92b0d feat: use sorry if failed to synthesize default element for unsafe constant 2022-04-05 16:52:54 -07:00
Leonardo de Moura
5470100830 feat: better binder names at reorderCtorArgs 2022-04-03 10:03:47 -07:00
Leonardo de Moura
61ae72330f feat: improve universe level contraint checks in inductive datatype constructors 2022-04-03 09:19:22 -07:00
Leonardo de Moura
3ee8ceafb4 feat: better error message when constructor parameter universe level is too big 2022-04-03 08:37:38 -07:00
Leonardo de Moura
ef8fecff79 feat: add Level.geq 2022-04-03 08:18:14 -07:00
Leonardo de Moura
310961cc35 chore: add scaffolding for checking ctor universe params 2022-04-03 07:33:02 -07:00
Leonardo de Moura
743f6dd3a2 chore: cleanup 2022-04-03 06:56:27 -07:00
Leonardo de Moura
2c7c7471db feat: add case' tactic for writing macros 
It is similar to `case` but does not admit goal in case of failure.
This is useful for writing macros.
 2022-04-02 17:54:06 -07:00
Leonardo de Moura
4fa5f50559 feat: implement TODO at "fixed indices to parameters" 
The missing feature (TODO in the code) is needed for the `BinTree` example.
 2022-04-02 14:37:24 -07:00
Leonardo de Moura
9fe5458077 feat: do not display inaccessible proposition names if they do not have forward dependencies 
Even if `pp.inaccessibleNames = true`
 2022-04-02 13:15:17 -07:00
Leonardo de Moura
95bd55bc21 chore: fix typo and remove unnecessary discriminant 2022-04-02 13:15:17 -07:00
Leonardo de Moura
be014b1fc9 fix: dotted notation corner case 2022-04-01 18:20:44 -07:00
Leonardo de Moura
a926cd1698 fix: mkUnfoldProof 
The hypotheses in an equation theorem may depend on each other
 2022-04-01 15:47:24 -07:00
Leonardo de Moura
4a0f68de83 fix: split tactic issue 2022-04-01 15:47:24 -07:00
Leonardo de Moura
ea8f31144e feat: add predicate to generalize tactic to select subterms to be generalized 2022-04-01 15:47:24 -07:00
Leonardo de Moura
fdd1cb5751 chore: remove workarounds for #1090 2022-04-01 11:28:17 -07:00
Leonardo de Moura
48a3668780 chore: fix repo 2022-04-01 11:24:30 -07:00
Leonardo de Moura
799c701f56 fix: inconsistency between syntax and kind names 
TODO: remove staging workarounds

see #1090
 2022-04-01 11:20:16 -07:00
Leonardo de Moura
68acfc7fb9 chore: prepare for #1090 2022-04-01 11:11:28 -07:00
Leonardo de Moura
09de67780f chore: prepare for #1090 2022-04-01 09:35:06 -07:00
Leonardo de Moura
92382ea47b fix: checkpoint 2022-04-01 05:53:18 -07:00
Leonardo de Moura
4c9c62752e feat: improve checkpoint tactic 2022-03-31 20:51:53 -07:00
Leonardo de Moura
23f41fddb3 feat: basic tactic cache 
TODO: move `IO.Ref` to command
 2022-03-31 19:53:03 -07:00
Leonardo de Moura
059459b097 fix: occurs check at refine tactic 2022-03-31 18:08:05 -07:00
Leonardo de Moura
87db7a9115 chore: style 2022-03-31 17:33:56 -07:00
Leonardo de Moura
096e4eb6d0 fix: equation generation for nested recursive definitions 
The issue was raised on Zulip. The issue is triggered in
declarations containing overlapping patterns and nested recursive
definitions occurring as the discriminant of `match`-expressions.
Recall that Lean 4 generates conditional equations for declarations
containing overlapping patterns.
To address the issue we had to "fold" `WellFounded.fix` applications
back as recursive applications of the functions being defined.

The new test exposes the issue.
 2022-03-31 17:04:06 -07:00
Leonardo de Moura
d21e62ecb7 refactor: custom simpMatch for WF module 
It is just the skeleton right now.
 2022-03-31 14:51:07 -07:00
Leonardo de Moura
1ab57d4fd4 feat: store fixedPrefixSize at WF.EqnInfo 2022-03-31 14:47:52 -07:00
Leonardo de Moura
23f3de5061 chore: proper trace message class 2022-03-31 11:04:42 -07:00
Leonardo de Moura
3dd0c84c4d chore: enforce naming convetion for tactics 2022-03-30 16:19:05 -07:00
Leonardo de Moura
46ce3013d0 feat: cleanup local context before elaborating match alternatives RHS 2022-03-29 18:52:07 -07:00
Leonardo de Moura
d1e4712038 fix: smart unfolding 
See new comment to understand the issue.

closes #1081
 2022-03-29 15:49:14 -07:00
Leonardo de Moura
a8bb7fab93 fix: typo at findRecArg 
The code was not traversing the indices if the datatype has parameters
 2022-03-29 12:12:43 -07:00
Leonardo de Moura
86432f1833 feat: improve let-pattern and have-pattern macro expansion 2022-03-29 07:33:22 -07:00