Sebastian Ullrich
bb738796ae
test: update parser benchmark, add to speedcenter suite
2023-08-08 18:40:19 +02:00
Sebastian Ullrich
8fc1af650a
fix: symmetry in orelse antiquotation parsing
2023-07-28 08:36:33 -07:00
Sebastian Ullrich
aeb60764c1
feat: auto-complete declaration names in arbitrary namespaces
2023-07-28 07:50:09 -07:00
Sebastian Ullrich
e84ce2e1f1
test: make completion tests less dependent on core
2023-07-28 07:50:09 -07:00
Sebastian Ullrich
b15d6d41b8
fix: missing mkCIdents in Lean.Elab.Deriving.Util
2023-07-28 07:48:34 -07:00
Sebastian Ullrich
d991f5efe0
fix: ship libLake.a
2023-07-21 09:19:19 +02:00
Sebastian Ullrich
d62fca4e9c
chore: safer bench script
2023-07-19 08:31:39 +02:00
Floris van Doorn
1a6663a41b
chore: write "|-" as "|" noWs "-" ( #2299 )
...
* remove |- as an alias for ⊢
* revert false positive |->
* fix docstring
* undo previous changes
* [unchecked] use suggestion
* next attempt
* add test
2023-07-14 09:48:20 -07:00
Scott Morrison
0d5c5e0191
feat: relax test in checkLocalInstanceParameters to allow instance implicits
2023-07-13 10:54:06 -07:00
Leonardo de Moura
fd0549feb5
chore: improve test
2023-07-11 19:19:42 -07:00
Leonardo de Moura
6d857a93b5
perf: pointer set for traversing DAGs
2023-07-11 19:19:42 -07:00
Leonardo de Moura
5402c3cf76
chore: fix test file names
2023-07-01 06:20:36 -07:00
Mario Carneiro
f1b2a8acce
fix: lazy_binop + coercion bug
...
fixes #2300
2023-07-01 06:05:25 -07:00
Leonardo de Moura
94d4a427e2
fix: fixes #2115
2023-06-30 19:54:38 -07:00
Leonardo de Moura
a002ce6d0d
fix: fixes #2077
2023-06-30 19:26:00 -07:00
Leonardo de Moura
ec42581d1f
perf: use Core.transform instead of Meta.transform at betaReduceLetRecApps
...
Observed big performance improvement on files containing big proofs
generated using tactics.
2023-06-28 12:29:12 -07:00
Leonardo de Moura
eece499da9
fix: fixes #2282
2023-06-27 16:46:38 -07:00
Leonardo de Moura
2b8e55c2f1
fix: Nat literal bug at DiscrTree.lean
2023-06-21 20:28:17 -07:00
Scott Morrison
a44dd71ad6
feat: add flag for apply to defer failed typeclass syntheses as goals
2023-06-19 20:07:07 -07:00
Scott Morrison
82196b5b94
feat: allow upper case single character identifiers when relaxedAutoImplicit false ( #2277 )
...
* feat: allow upper case single character identifiers when relaxedAutoImplicit false
* update tests
* fix tests
* fix another test
---------
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
2023-06-19 20:04:09 -07:00
Gabriel Ebner
bff612e59e
fix: simp: synthesize non-inst-implicit tc args
...
Fixes #2265 .
2023-06-09 16:32:02 -07:00
Mario Carneiro
1ac8a4083f
feat: report section name in invalid end msg
2023-06-09 14:41:39 -07:00
Mario Carneiro
b4cf1dd943
feat: binder info for generalize
2023-06-09 14:41:00 -07:00
Mario Carneiro
b139a97825
fix: hygieneInfo should not consume whitespace
2023-06-09 15:05:19 +02:00
Sebastian Ullrich
451ccec154
fix: save when used as last tactic
2023-06-07 14:29:45 -07:00
Sebastian Ullrich
97cffd4711
fix: prefer resolving parser alias over declaration
2023-06-05 16:52:23 +02:00
Mario Carneiro
a8d6178e19
feat: implement have this (part 2)
2023-06-02 16:19:02 +02:00
Mario Carneiro
c20a7bf305
feat: hygieneInfo parser (aka this 2.0)
2023-06-02 16:19:02 +02:00
Mario Carneiro
e826f5f42a
fix: spacing around calc
2023-06-02 09:15:15 +02:00
Mario Carneiro
5661b15e35
fix: spacing and indentation fixes
2023-05-28 18:48:36 -07:00
Leonardo de Moura
83cc0bcc96
fix: fixes #2199
2023-05-28 18:29:09 -07:00
Jannis Limperg
c84690028b
fix: ignore implDetail hyps in withLocation
2023-05-28 17:40:55 -07:00
Mario Carneiro
5d3ac5f80c
fix: panic in Match.SimpH.substRHS
2023-05-28 17:04:28 -07:00
Gabriel Ebner
ebc32af2e6
chore: fix flaky test
2023-05-15 13:23:38 -07:00
Parth Shastri
555f5f390c
fix: stop iterating over visited mvars in collectUnassignedMVars
2023-05-15 09:37:19 -07:00
Parth Shastri
954190e457
fix: remove repeat calls to inferType in ignoreField
2023-05-15 09:35:44 -07:00
Gabriel Ebner
5781752985
fix: offset unification with a+a+1
...
Fixes #2136
2023-05-15 09:06:37 -07:00
Gabriel Ebner
ae2b2c3903
chore: add regression test for mathlib eta perf issue
2023-05-15 09:05:41 -07:00
Gabriel Ebner
1f21ababfa
chore: remove etaExperiment option
2023-05-15 09:05:41 -07:00
Gabriel Ebner
41729263c5
fix: tests
2023-05-15 09:05:41 -07:00
Mario Carneiro
ad4b822734
fix: use snake case for @[code_action_provider]
2023-05-08 22:25:48 +02:00
Henrik Böving
0e042d8ef6
fix: LCNF simp forgot to mark normalized decls as simplified
2023-05-05 12:17:26 -07:00
Henrik Böving
a6ae661195
feat: profiling of linters
2023-04-18 15:30:21 +02:00
Sebastian Ullrich
8a302e6135
fix: match discriminant reduction should not unfold irreducible defs
2023-04-10 21:09:04 -07:00
Gabriel Ebner
7f51628986
fix: simp: strip mdata when testing for True/False
...
Fixes #2173
2023-04-10 21:06:42 -07:00
Scott Morrison
06c752448b
chore: add missing simp lemma (¬ False) = True
2023-04-10 21:05:54 -07:00
Gabriel Ebner
8075d1f45d
fix: reset local context in mkInjectiveTheorems
2023-04-10 21:05:16 -07:00
Gabriel Ebner
5eb9688846
chore: flaky tests
2023-04-10 13:00:04 -07:00
Gabriel Ebner
4544443d98
feat: reorder tc subgoals according to out-params
2023-04-10 13:00:04 -07:00
Sebastian Ullrich
427540db45
chore: remove redundant Elab.input trace class in favor of Elab.command
2023-04-10 16:57:54 +02:00
