Leonardo de Moura
|
9a16d4afce
|
feat: add CompilerM.lean and LCNF.lean
|
2022-08-05 21:14:39 -07:00 |
|
Chris Lovett
|
c4121e779d
|
fix: hexDigit ('a' ≤ c ∧ c ≤ 'f')
|
2022-08-05 14:08:03 -07:00 |
|
Leonardo de Moura
|
deafc315c7
|
fix: make forall_congr more robust at conv intro
closes #1426
|
2022-08-05 12:38:49 -07:00 |
|
Mario Carneiro
|
ea0f177bf2
|
feat: add unused/deprecation diagnostic tags
|
2022-08-05 17:45:50 +02:00 |
|
Leonardo de Moura
|
7f9be4198b
|
fix: Induction.lean after binderIdent normalization
|
2022-08-04 21:28:12 -07:00 |
|
Leonardo de Moura
|
55bb8e905a
|
chore: binderIdent normalization
fixes #1411
|
2022-08-04 21:10:02 -07:00 |
|
Mario Carneiro
|
c1d2f3c5a6
|
feat: make MissingDocs extensible
|
2022-08-04 19:35:00 -07:00 |
|
Mario Carneiro
|
eef51aced2
|
feat: make MissingDocs extensible (part 1)
|
2022-08-04 19:32:17 -07:00 |
|
Leonardo de Moura
|
f0272d9309
|
feat: multiple namespaces in mutual declarations
|
2022-08-04 19:18:49 -07:00 |
|
Leonardo de Moura
|
16d6f13eed
|
chore: fix warnings
|
2022-08-04 16:05:09 -07:00 |
|
Leonardo de Moura
|
0717bdb66d
|
fix: fixes #1419
|
2022-08-04 15:44:38 -07:00 |
|
Leonardo de Moura
|
4501bdecb1
|
chore: naming convention
|
2022-08-04 15:28:22 -07:00 |
|
Sebastian Ullrich
|
2f0b65fad3
|
fix: do not show inaccessible variable in hover
|
2022-08-04 11:28:46 -07:00 |
|
Leonardo de Moura
|
a30a31b1b0
|
fix: findDocString?
|
2022-08-04 10:32:41 -07:00 |
|
Leonardo de Moura
|
85cda05c92
|
chore: improve expandParen do notation
|
2022-08-04 10:01:32 -07:00 |
|
Leonardo de Moura
|
0ec56c3367
|
chore: fix doc string
|
2022-08-04 08:45:30 -07:00 |
|
Leonardo de Moura
|
1008607b25
|
chore: cleanup annotate method at Do.lean
|
2022-08-04 08:44:56 -07:00 |
|
Sebastian Ullrich
|
abde2e4606
|
fix: unused variables in foreign definition
|
2022-08-03 18:15:15 -07:00 |
|
Mario Carneiro
|
e816424466
|
chore: use Category declarations for builtin cats too (#1400)
|
2022-08-03 18:10:54 -07:00 |
|
Leonardo de Moura
|
84ff8d4a04
|
feat: store pending contraints during dependent pattern matching
It is a better solution for issues #1361 and #1279, and it was on the
to-do list for a while.
|
2022-08-03 17:45:55 -07:00 |
|
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 |
|