Leonardo de Moura
d61b8fc68d
test: for LCNF types
2022-08-10 11:07:13 -07:00
Gabriel Ebner
e9545a426f
refactor: RpcEncodable
2022-08-10 06:31:46 -07:00
Gabriel Ebner
067f8e6449
feat: Std.TypeName and Std.Dynamic
2022-08-10 06:31:46 -07:00
Mario Carneiro
0c3383c0b0
feat: support let mut x := e | alt
2022-08-10 06:29:49 -07:00
Mario Carneiro
a28c19c161
doc: improve typeclass ops documentation
2022-08-09 14:25:44 -07:00
Mario Carneiro
6026894f9f
doc: finish Init.Prelude docs
2022-08-09 14:25:44 -07:00
Leonardo de Moura
3c6c395e44
feat: add TerminalCases.lean
2022-08-07 22:05:19 -07:00
Leonardo de Moura
7dbfaf9b75
fix: bug at mkSizeOfSpecLemmaInstance
...
closes #1441
2022-08-07 09:24:18 -07:00
Mario Carneiro
0b92f625ae
feat: MissingDocs doesn't lint on struct redecl
2022-08-07 08:48:42 -07:00
Leonardo de Moura
413db56b89
refactor: simplify runTermElabM and liftTermElabM
2022-08-07 07:35:02 -07:00
Leonardo de Moura
ee70805c35
feat: add LCNF missing cases
2022-08-06 20:23:29 -07:00
Mario Carneiro
37d3479e7c
doc: add more docs to Init.Prelude
2022-08-06 09:32:16 -07:00
Sebastian Ullrich
3ee9ab855e
fix: logging of linter warnings
2022-08-06 09:25:09 -07:00
Leonardo de Moura
4167b2466a
fix: improve heuristic for issue #1419
...
The fix #1419 generated two regressions on Mathlib.
Fixes #1435
Fixes #1436
2022-08-06 09:00:16 -07:00
Leonardo de Moura
386b0a75bc
fix: bug at lean_nat_mod
...
fixes at #1433
2022-08-06 08:07:25 -07:00
Leonardo de Moura
bf59ad0efc
feat: add new compiler entry point function
2022-08-06 08:05:07 -07:00
Mario Carneiro
59b32da2d9
feat: go to def on parser aliases
2022-08-06 12:44:14 +02:00
Leonardo de Moura
9a16d4afce
feat: add CompilerM.lean and LCNF.lean
2022-08-05 21:14:39 -07:00
Leonardo de Moura
ddeea5e14f
chore: fix test output
2022-08-05 13:01:02 -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
Leonardo de Moura
50cecdbb62
chore: add Inhabited MProd and Inhabited PProd instances
...
closes #1420
2022-08-05 11:21:27 -07: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
Leonardo de Moura
659300597d
doc: some doc strings for Prelude.lean
2022-08-04 20:55:13 -07:00
Mario Carneiro
e2f706a7f7
fix: syntax match
2022-08-04 19:35:00 -07:00
Mario Carneiro
c1d2f3c5a6
feat: make MissingDocs extensible
2022-08-04 19:35:00 -07:00
Leonardo de Moura
f0272d9309
feat: multiple namespaces in mutual declarations
2022-08-04 19:18:49 -07:00
Leonardo de Moura
0717bdb66d
fix: fixes #1419
2022-08-04 15:44:38 -07:00
Leonardo de Moura
f295a76b69
chore: fix test output
2022-08-04 15:29:17 -07:00
Leonardo de Moura
8615c42a5d
tests: projection defeq strategy
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
Mario Carneiro
f5c5af1e86
doc: document all the syntax categories ( #1401 )
...
* chore: use Category declarations for builtin cats too
* doc: document all the syntax categories
* fix: fix test
2022-08-03 18:13:39 -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
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
fbef8a32e1
feat: add support for stuck class projection function applications at getStuckMVar?
...
closes #1408
2022-08-02 16:01:06 -07:00
Sebastian Ullrich
a44472962d
fix: replace uses of token antiquotations in tactics with with_annotate_state
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
3ab26f00ea
refactor: use congr tactic to implement the congr conv tactic
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
815bc95c47
refactor: remove duplication MVarId.applyRefl => MVarId.refl
...
and mark `MVarId.applyRefl` as deprecated.
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
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
5a8ee410b1
chore: remove infoTree.lean test
...
Motivation: it is not very useful anymore, and more importantly it
breaks all the time because it is affected by how many internal ids
are created by Lean.
2022-08-01 10:02:24 -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
c952c69690
feat: add missingDocs linter
2022-07-31 18:18:21 -07:00
Mario Carneiro
7cefcf1f61
fix: fix test
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
