Scott Morrison
4a41e7eb53
chore: basic tests exercising rw
2023-08-29 08:07:58 +01:00
thorimur
0b64c1e330
fix: make sure refine preserves pre-existing natural mvars ( #2435 )
...
* fix: `withCollectingNewGoals`
* don't exclude pre-existing natural mvars
* test: ensure pre-existing natural mvars are preserved
* docs: update comment and include issue number
* test: expected.out
* docs: add module docstrings to test
* also deleted superfluous `add_synthetic_goal`
* test: fix expected.out line numbers
* Update tests/lean/refinePreservesNaturalMVars.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* docs: clarify comment
---------
Co-authored-by: Scott Morrison <scott@tqft.net>
2023-08-25 19:25:54 -07:00
Scott Morrison
f1412ddb45
feat: enable failIfUnchanged by default in simp
2023-08-16 10:14:23 -07:00
Scott Morrison
58d19b80b9
test: compiling from the interpreter, with common imports
...
hacky fix to windows test
Include test from #2407 as well
2023-08-16 10:11:50 -07:00
Siddharth Bhat
146296b5fa
feat: enable LLVM in stage1+ compiler
2023-08-14 13:33:46 +02:00
Scott Morrison
61fea57e73
feat: add failIfUnchanged flag to simp
2023-08-13 09:49:25 -07:00
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
