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
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
