Leonardo de Moura
f2921993bb
feat: add LocalContext.replaceFVarId
2022-08-03 11:21:55 -07:00
Leonardo de Moura
cbd022e4eb
refactor: replaceFVarIdAtLocalDecl => LocalDecl.replaceFVarId
2022-08-03 10:32:45 -07:00
Leonardo de Moura
b4ad6fc289
chore: do not generate "redundant alternatives" message when there are missing cases
2022-08-03 08:21:09 -07:00
Leonardo de Moura
a9e7290e4b
refactor: use isDefEq instead of custom unify procedure
...
See comment with new issue at #1361
2022-08-02 18:00:00 -07:00
Leonardo de Moura
ae5db0f563
chore: style
2022-08-02 17:44:19 -07:00
Leonardo de Moura
fbef8a32e1
feat: add support for stuck class projection function applications at getStuckMVar?
...
closes #1408
2022-08-02 16:01:06 -07:00
Leonardo de Moura
40226f775f
chore: doc strings for ProjFns.lean
2022-08-02 15:58:56 -07:00
Leonardo de Moura
9d36f45074
chore: cleanup
2022-08-02 14:45:19 -07:00
Leonardo de Moura
2e37582f31
feat: allow users to install their own deriving hanlders for builtin classes
2022-08-02 08:29:24 -07:00
Sebastian Ullrich
8b235579e3
fix: ignore with_annotate_state for hover/go-to
2022-08-02 04:54:48 -07:00
Sebastian Ullrich
0272c30b4b
fix: token antiquotations should create synthetic positions
...
synthetic means synthetic means synthetic
2022-08-02 04:54:48 -07:00
Leonardo de Moura
303e322255
feat: avoid [Decidable p] instance implicit parameters in congruence theorems when possible
2022-08-02 04:47:42 -07:00
Leonardo de Moura
b2f34bdedd
feat: improve congr conv tactic
...
It has better support for proof irrelevant and `[Decidable p]` arguments
2022-08-02 04:26:34 -07:00
Leonardo de Moura
01ce4b9982
feat: use infer_instance to close remaining goals at conv block
2022-08-02 04:24:56 -07:00
Leonardo de Moura
c143631ab1
chore: missing instantiateMVars
2022-08-02 02:24:50 -07:00
Leonardo de Moura
e6d5349abb
chore: unused variable
2022-08-02 02:24:50 -07:00
Leonardo de Moura
3ab26f00ea
refactor: use congr tactic to implement the congr conv tactic
2022-08-02 02:24:50 -07:00
Leonardo de Moura
e79917d9a8
fix: missing instantiateMVars
2022-08-02 02:24:50 -07:00
Leonardo de Moura
4e911765eb
chore: unused vars
2022-08-02 02:24:50 -07:00
Leonardo de Moura
076d40f51c
feat: use implies_congr at congr tactic, and cleanup
2022-08-02 02:24:50 -07:00
Leonardo de Moura
99413a18ff
feat: add congr tactic
2022-08-01 18:44:07 -07:00
Leonardo de Moura
cdd2a624fc
fix: mkHCongr
2022-08-01 18:44:07 -07:00
Leonardo de Moura
815bc95c47
refactor: remove duplication MVarId.applyRefl => MVarId.refl
...
and mark `MVarId.applyRefl` as deprecated.
2022-08-01 18:44:07 -07:00
Leonardo de Moura
a5a70a0543
chore: cleanup
2022-08-01 18:44:07 -07:00
Mario Carneiro
5f39370d94
chore: rename skip conv to rfl and add no-op skip
2022-08-01 13:54:36 -07:00
Leonardo de Moura
e39eebabd9
fix: move doc string to parser that sets the SyntaxNodeKind for the { tac } notation
...
see #1403
This fixes the hover for `{ tac }`
2022-08-01 13:01:37 -07:00
Leonardo de Moura
c95acef20e
fix: ignore syntax nodes with nullKind at hoverableInfoAt?
...
It fixes one of the problems reported at #1403
2022-08-01 12:18:36 -07:00
Leonardo de Moura
2af7bf1b54
chore: fix link at src/Lean/Server/README.md
...
cc @digama0
2022-08-01 11:12:19 -07:00
Leonardo de Moura
0156b59ef1
chore: enforce naming convention
2022-08-01 09:58:11 -07:00
Mario Carneiro
25aea1b723
doc: document all the tactics
2022-08-01 08:08:03 -07:00
Sebastian Ullrich
de029566d1
fix: unused variables false positive with match
2022-08-01 07:09:08 -07:00
Mario Carneiro
df85fee62c
chore: rename ac_refl to ac_rfl
2022-08-01 06:53:08 -07:00
Mario Carneiro
114cd3e5cd
doc: add ParserCategory docs
2022-08-01 11:23:09 +02:00
Mario Carneiro
ecb787529a
refactor: rename ref to declName
2022-08-01 11:23:09 +02:00
Mario Carneiro
711532f5c6
feat: add ref field to ParserCategory
2022-08-01 11:23:09 +02:00
Mario Carneiro
65e2b8a932
feat: track parser names by category
2022-08-01 11:23:09 +02:00
Mario Carneiro
c952c69690
feat: add missingDocs linter
2022-07-31 18:18:21 -07:00
Mario Carneiro
89a16daa81
feat: add TokenMap
2022-07-31 15:42:26 -07:00
Mario Carneiro
42a4f2f451
feat: ForIn instance for NameMap and PersistentHashMap
2022-07-31 15:42:26 -07:00
Leonardo de Moura
8241c49e11
fix: variable binder update commands
...
This issue was reported by @hrmacbeth at the ICERM after-party hackton.
2022-07-31 10:08:48 -07:00
Sebastian Ullrich
759a7d771f
fix: do not show inferred type on attribute application
2022-07-31 16:36:54 +02:00
Mario Carneiro
603b7486e3
feat: add go-to-def for simple attributes
2022-07-31 16:36:54 +02:00
Leonardo de Moura
37af11ae20
fix: unused match-syntax alternatives are silently ignored
...
closes #1371
2022-07-31 06:00:08 -07:00
Leonardo de Moura
feb71271e9
fix: remove redundant alternatives
2022-07-31 05:28:14 -07:00
Leonardo de Moura
2f00d60115
feat: helper parser for issue #1371
2022-07-31 04:30:02 -07:00
Leonardo de Moura
cc032446f4
chore: style
2022-07-30 21:29:12 -07:00
Leonardo de Moura
4c1387b99b
chore: typos
2022-07-30 21:26:08 -07:00
Siddharth
68e26278c7
doc: Add explanations to MetavarContext ( #1331 )
...
* doc: Add explanations to MetavarContext
The explanations were taken from Leo's talk at the ICERM
Mathlib porting hackathon.
* Update src/Lean/MetavarContext.lean
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* add my understanding of what LocalInstances represents
* Update src/Lean/MetavarContext.lean
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>
2022-07-30 21:24:42 -07:00
Leonardo de Moura
a489bdb107
doc: some doc strings
2022-07-30 21:18:50 -07:00
Leonardo de Moura
ab6af0118c
doc: add inductive command doc string
2022-07-30 15:15:16 -07:00
