Sebastian Ullrich
|
2070df2328
|
feat: check task cancellation in elaborator
|
2023-10-13 09:52:26 +02:00 |
|
Scott Morrison
|
ca0e6b0522
|
chore: fix MVarId.getType' (#2595)
* chore: fix MVarId.getType'
* add test
|
2023-10-09 11:04:33 +00:00 |
|
Sebastian Ullrich
|
00e981edcd
|
perf: do not inhibit caching of default-level match reduction
|
2023-10-08 17:24:20 -07:00 |
|
Leonardo de Moura
|
9f50f44eed
|
perf: missing cache at whnfImp
|
2023-10-08 17:22:14 -07:00 |
|
int-y1
|
8d7520b36f
|
chore: fix typos in comments
|
2023-10-08 10:46:05 +02:00 |
|
Arthur Adjedj
|
325fab1c1d
|
fix: don't try to generate below for nested predicates. (#2390)
* fix: don't try to generate `below` for nested predicates.
* doc : document test #2389
* doc : document `mkBelow`
* test: extend `2389.lean`
* style: fix comments in `IndPredBelow.lean` and `2389.lean`
|
2023-09-21 14:24:37 +10:00 |
|
Scott Morrison
|
c318d5817d
|
feat: allow configuring occs in rw
|
2023-09-13 12:03:18 -07:00 |
|
Jannis Limperg
|
13ca443f05
|
fix: simp: include class projections in UsedSimps (#2489)
* fix: simp: include class projections in UsedSimps
Fixes #2488
|
2023-09-07 08:54:00 +10:00 |
|
Jannis Limperg
|
9a262d7cef
|
fix: simpGoal reports incomplete UsedSimps (#2487)
|
2023-09-01 10:20:49 +10:00 |
|
Scott Morrison
|
1dd443a368
|
doc: improve doc-string for Meta.getConst?
|
2023-08-24 07:42:28 -07:00 |
|
Scott Morrison
|
61fea57e73
|
feat: add failIfUnchanged flag to simp
|
2023-08-13 09:49:25 -07:00 |
|
Jannis Limperg
|
6407197e54
|
chore: better error message for loose bvar in whnf
|
2023-07-20 13:47:20 -07:00 |
|
Leonardo de Moura
|
94d4a427e2
|
fix: fixes #2115
|
2023-06-30 19:54:38 -07:00 |
|
Leonardo de Moura
|
eece499da9
|
fix: fixes #2282
|
2023-06-27 16:46:38 -07:00 |
|
Sebastian Ullrich
|
f0583c3fd6
|
feat: trace nodes for SizeOf and injectivity theorem generation
|
2023-06-27 16:17:46 -07:00 |
|
Leonardo de Moura
|
425f42cd83
|
feat: better support for Nat literals at DiscrTree.lean
|
2023-06-21 22:30:09 -07:00 |
|
Leonardo de Moura
|
184f2ed597
|
chore: improve isNonTrivialProof
|
2023-06-21 20:28:17 -07:00 |
|
Leonardo de Moura
|
7367f2edc6
|
fix: unfold constant theorems when transparency is set to .all
|
2023-06-21 20:28:17 -07:00 |
|
Leonardo de Moura
|
9df2f6b0c9
|
fix: bump transparency to .all when reducing the major premise of Acc.rec and WellFounded.rec
|
2023-06-21 20:28:17 -07:00 |
|
Leonardo de Moura
|
2b8e55c2f1
|
fix: Nat literal bug at DiscrTree.lean
|
2023-06-21 20:28:17 -07:00 |
|
Leonardo de Moura
|
d6695a7a2e
|
fix: use mkAuxTheoremFor when creating helper proof_n theorems
|
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 |
|
Gabriel Ebner
|
bff612e59e
|
fix: simp: synthesize non-inst-implicit tc args
Fixes #2265.
|
2023-06-09 16:32:02 -07:00 |
|
Leonardo de Moura
|
25384fe951
|
fix: fixes #2232
|
2023-05-31 05:48:25 -07:00 |
|
Leonardo de Moura
|
e04d67f55f
|
chore: expand docstring for TransformStep.visit
|
2023-05-31 05:48:25 -07:00 |
|
Mario Carneiro
|
9ec9ea61a4
|
fix: infinite loop in isClassApp?
|
2023-05-30 18:47:17 -07:00 |
|
Leonardo de Moura
|
83cc0bcc96
|
fix: fixes #2199
|
2023-05-28 18:29:09 -07:00 |
|
Mario Carneiro
|
5d3ac5f80c
|
fix: panic in Match.SimpH.substRHS
|
2023-05-28 17:04:28 -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
|
1f21ababfa
|
chore: remove etaExperiment option
|
2023-05-15 09:05:41 -07:00 |
|
Gabriel Ebner
|
8de8c80119
|
perf: do not unify proof arguments
|
2023-05-15 09:05:41 -07:00 |
|
Gabriel Ebner
|
89cb94fcab
|
perf: try structure eta after delta
|
2023-05-15 09:05:41 -07:00 |
|
Gabriel Ebner
|
9211dd6541
|
chore: tc: re-enable eta
|
2023-05-15 09:05:41 -07:00 |
|
Jakob von Raumer
|
45b49e7f02
|
fix: typos
|
2023-05-05 12:07:54 -07: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 |
|
Gabriel Ebner
|
8075d1f45d
|
fix: reset local context in mkInjectiveTheorems
|
2023-04-10 21:05:16 -07:00 |
|
Gabriel Ebner
|
4af329588e
|
doc: clarify semi-out params
|
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
|
b076d488e3
|
feat: show typeclass and tactic names in profile output
|
2023-03-27 17:47:52 +02:00 |
|
Gabriel Ebner
|
8650804b02
|
perf: cache tc results with mvars
|
2023-03-16 15:26:38 -07:00 |
|
Gabriel Ebner
|
d3c55ef249
|
perf: do not reset tc cache when adding local instances
|
2023-03-16 15:26:38 -07:00 |
|
Gabriel Ebner
|
0cc9d7a43d
|
fix: do not reverse subgoals of local instances
|
2023-03-08 15:54:07 -08:00 |
|
Gabriel Ebner
|
2262579f9b
|
fix: tc: filter out assigned subgoals at the correct place
|
2023-03-08 15:54:07 -08:00 |
|
Gabriel Ebner
|
3ab859553e
|
fix: allow function coercion to assign universe mvars
|
2023-03-08 15:54:07 -08:00 |
|
Gabriel Ebner
|
1c641b569a
|
chore: synthInstance trace message on cache hit
|
2023-03-08 15:54:07 -08:00 |
|
Gabriel Ebner
|
1f61633da7
|
fix: typo in trace class name
|
2023-03-08 15:54:07 -08:00 |
|
Gabriel Ebner
|
adcca17991
|
chore: add option to enable structure eta in tc search
|
2023-02-21 16:41:30 -08:00 |
|
Gabriel Ebner
|
75252d2b85
|
perf: whnf projections during defeq
|
2023-02-09 19:54:23 -08:00 |
|