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

4403 commits

Author SHA1 Message Date
Leonardo de Moura
4dd2b26e06 fix: rfl error message and corner case 
The new `rfl` slightly improves the performance for `rfl` proofs of
ground terms.
Example: `state8.lean` now takes 0.37s. It was 0.52s.
 2022-04-09 12:08:04 -07:00
Leonardo de Moura
03f6b87647 feat: add hand-written rfl tactic 
It requires update stage0
 2022-04-09 11:57:27 -07:00
Leonardo de Moura
298281baaf perf: skip logUnassignedUsingErrorInfos if pendingMVarIds is empty 
`state8.lean` now takes 0.52s. It was 0.76s.
 2022-04-09 10:45:52 -07:00
Leonardo de Moura
7d99f6f555 perf: isClassQuick? was incorrectly producing undef 
Then `isClassExpensive?` was being invoked too often. In some
benchmarks the performance hit was substantial. For example,
in the new test `state8.lean`. The runtime on my machine went from 2s
to 0.76s.
 2022-04-09 10:38:49 -07:00
Leonardo de Moura
6e02514eee chore: style 2022-04-09 10:27:31 -07:00
Leonardo de Moura
417421dbae fix: auto completion when autoBoundImplicit is active 2022-04-09 09:11:45 -07:00
Leonardo de Moura
87e6581e6b fix: constructor elaboration 
fixes #1098
 2022-04-08 18:19:06 -07:00
Leonardo de Moura
3cf425ba52 fix: pattern hover information 
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
 2022-04-08 15:03:42 -07:00
Leonardo de Moura
4793c7e734 feat: add isAppOfArity variant that skips Expr.mdata 2022-04-08 15:01:57 -07:00
Leonardo de Moura
152eff5cea chore: missing double ticks 2022-04-08 15:01:57 -07:00
Leonardo de Moura
ea682830d1 refactor: change addTermInfo type 2022-04-08 15:01:57 -07:00
Leonardo de Moura
5d8b4f33c0 feat: improve binder names introduced by the match discriminant refinement feature 2022-04-08 06:49:09 -07:00
Leonardo de Moura
099fba43d3 chore: remove trace[Meta.debug] leftovers 2022-04-08 06:49:09 -07:00
E.W.Ayers
917fa74366 doc: docstrings for decls and attributes 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-04-08 04:19:38 -07:00
Leonardo de Moura
cec0f81926 chore: add instantiateMVars 2022-04-07 18:46:45 -07:00
Leonardo de Moura
37b321229f feat: make sure hover information does not include @ for constants 2022-04-07 18:40:04 -07:00
Leonardo de Moura
55989c25fc chore: remove unnecessary args 2022-04-07 18:19:15 -07:00
Leonardo de Moura
de2e2447d2 chore: style 2022-04-07 17:35:05 -07:00
Leonardo de Moura
dcb88d969a feat: improve auto implicit binder names in definitions/theorems 2022-04-07 14:46:59 -07:00
Leonardo de Moura
cd0d7e676f chore: rename renameMVar => setMVarUserName 2022-04-07 13:50:58 -07:00
Leonardo de Moura
00c4524e80 chore: register Elab.induction trace class 2022-04-07 13:22:40 -07:00
Leonardo de Moura
c26e968c24 chore: style 2022-04-07 11:25:45 -07:00
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