Mario Carneiro
c4cbefce11
feat: add linter.deprecated option to silence deprecation warnings
2022-10-23 21:11:57 +02:00
Gabriel Ebner
fc304d95c0
feat: Min/Max typeclasses
2022-10-21 14:36:38 -07:00
E.W.Ayers
112cb5e261
test: fix test output
2022-10-20 11:20:42 -07:00
E.W.Ayers
c9a26596dc
refactor: switch resolve to double eval strategy
...
Using option (2) from this comment:
https://github.com/leanprover/lean4/pull/1661#pullrequestreview-1135363727
2022-10-20 11:20:42 -07:00
E.W.Ayers
691835037e
feat: code action resolvers
2022-10-20 11:20:42 -07:00
E.W.Ayers
297d06fc0c
fix: issue where code action was not running
2022-10-20 11:20:42 -07:00
E.W.Ayers
8085ce88e9
feat: CodeActionProvider
...
This is a low-level system for registering LSP code actions.
Developers can register their own code actions.
In future commits I am going to add features on top of this.
2022-10-20 11:20:42 -07:00
Leonardo de Moura
aeddcbdc6d
fix: disable implicit lambdas at intro <pattern> notation
...
See issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/intro.20with.20type.20specified/near/305150215
2022-10-20 09:04:06 -07:00
Mario Carneiro
dd8bbe9367
fix: catch kernel exceptions in Kernel.{isDefEq, whnf}
...
fixes #1756
2022-10-20 05:38:29 -07:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Mario Carneiro
dd5948d641
chore: snake-case attributes (part 1)
2022-10-19 09:28:08 -07:00
Sebastian Ullrich
9fd433785b
chore: register pretty printer trace classes
2022-10-19 14:51:07 +02:00
Gabriel Ebner
0c2a5580cb
feat: enforce correct syntax kind in macros
2022-10-18 14:59:14 -07:00
Gabriel Ebner
fb4d90a58b
feat: dynamic quotations for categories
2022-10-18 14:59:14 -07:00
Leonardo de Moura
ec59bbe15c
chore: ensure LCNF pretty printer result supports Format.group
2022-10-16 16:06:08 -07:00
Leonardo de Moura
72c576f62a
feat: complete reduceArity pass
2022-10-16 16:00:33 -07:00
Leonardo de Moura
1a02c326e5
chore: fix test
2022-10-16 14:54:07 -07:00
Leonardo de Moura
9244a7a8a5
fix: ensure old and new compiler auxiliary declaration names do not collide
2022-10-16 14:49:55 -07:00
Leonardo de Moura
79ed382492
chore: fix test
2022-10-16 09:00:25 -07:00
Leonardo de Moura
c20febff31
feat: add helper Syntax.node* functions
2022-10-16 08:40:01 -07:00
Leonardo de Moura
b4d850502d
fix: avoid join point that takes closure at seqToCode
2022-10-15 15:48:02 -07:00
Leonardo de Moura
61813d60c6
test: for join point taking closure as parameter
2022-10-15 12:05:53 -07:00
Leonardo de Moura
376c541e9a
feat: do not generate code for declarations that will be specialized
2022-10-15 08:54:46 -07:00
Leonardo de Moura
6378283fa8
feat: add Probe.toString
2022-10-14 19:21:56 -07:00
Henrik Böving
38788a72be
feat: basic compiler probing framework with examples
2022-10-14 19:09:35 -07:00
Gabriel Ebner
1c561c39a8
feat: function coercions with unification
2022-10-14 12:08:10 -07:00
Mario Carneiro
0acdaddcf2
feat: unexpander for mkArray0
2022-10-14 08:51:45 -07:00
Rishikesh Vaishnav
76c4693c95
fix: improve fuzzy-matching heuristics ( #1710 )
2022-10-14 16:17:14 +02:00
Sebastian Ullrich
6b8fa76265
test: benchmark workspace symbols search
2022-10-13 21:41:58 +02:00
Leonardo de Moura
dfd95c712e
chore: fix tests
2022-10-13 06:16:56 -07:00
Leonardo de Moura
4ac802dd9a
chore: fix test
2022-10-13 04:31:46 -07:00
Leonardo de Moura
2675c0647b
feat: detect unreachable cases alternatives at LCNF simp
2022-10-13 02:49:55 -07:00
Sebastian Ullrich
e7b90b489a
fix: stabilize unused variables linter output
2022-10-13 10:46:53 +02:00
Gabriel Ebner
38d3e37c75
perf: improve Unhygienic.run code
2022-10-12 19:36:05 -07:00
Leonardo de Moura
49a6f8c105
chore: add horrible hack for Decidable in the new code generator
...
cc @gebner
2022-10-12 16:53:29 -07:00
Leonardo de Moura
7308fa0e7d
feat: ensure lambda lifter is creating unused names
2022-10-12 16:35:55 -07:00
Gabriel Ebner
79569c9003
chore: replace let by have in stx matches
2022-10-12 11:52:28 -07:00
Sebastian Ullrich
18a4b277fc
test: more fair qsort.ml benchmark
2022-10-12 20:22:55 +02:00
Mario Carneiro
8dfae9eb38
feat: import command stub
2022-10-12 11:11:31 -07:00
Leonardo de Moura
aa845dee98
feat: cache lambda lifted functions
2022-10-11 21:28:03 -07:00
Gabriel Ebner
15d7744cca
chore: fix tests
2022-10-11 17:24:35 -07:00
Gabriel Ebner
6593bd98b3
chore: add test for 1692
2022-10-11 17:24:35 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Mario Carneiro
f4b04216eb
feat: go to duplicate definition
2022-10-11 10:07:49 +02:00
Leonardo de Moura
525b4f761c
chore: fix tests
2022-10-10 17:48:32 -07:00
Henrik Böving
dd3c0f77f1
feat: FloatLetIn compiler pass
2022-10-10 23:56:20 +02:00
Leonardo de Moura
7b3709e28a
chore: simplify proof in test for #1711
...
TODO: improve support for instance implicit arguments at `congr`
2022-10-10 07:29:53 -07:00
Leonardo de Moura
0041de5d1d
fix: congr tactic should not try to synthesize instance implicit arguments that have been inferred when applying congr theorem
...
see #1711
2022-10-10 07:24:27 -07:00
Leonardo de Moura
fb4200e633
chore: fix tests
2022-10-09 21:51:51 -07:00
Leonardo de Moura
cc09afc5e1
fix: type error introducing when inlining LCNF functions
...
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/303142516
2022-10-09 12:10:11 -07:00
