Leonardo de Moura
a10e32f537
fix: check "heartbeats" at simp
2022-01-26 07:50:25 -08:00
Leonardo de Moura
15cca3000a
fix: withIncRecDepth was not aborting simp
...
It was just making it stop simplification at the current branch.
Now, elaboration is interrupted after a few seconds in the example at
issue #906 .
see #906
2022-01-26 07:48:58 -08:00
Leonardo de Moura
9c293abb9c
chore: expose heqToEq tactic
2022-01-25 18:43:51 -08:00
Leonardo de Moura
6547af988b
feat: add substVars
2022-01-25 18:43:51 -08:00
Leonardo de Moura
02677cf326
fix: igore instance implicit arguments in term ordering used at simp
...
closes #972
2022-01-24 18:57:31 -08:00
Leonardo de Moura
d4f7899591
chore: avoid code duplication setting Simp.Config
2022-01-24 18:57:31 -08:00
Leonardo de Moura
7ada79bf2e
fix: use an AC-compatible ordering on Expr at simp
...
closes #968
2022-01-22 09:42:59 -08:00
Leonardo de Moura
ef449e816f
chore: improve trace messages
2022-01-19 14:29:04 -08:00
Leonardo de Moura
c816524d8d
feat: add subst?
2022-01-18 14:26:14 -08:00
Leonardo de Moura
49b2860f2a
feat: add Meta.rename tactic
2022-01-12 16:15:30 -08:00
Leonardo de Moura
7a86b613dc
chore: remove old comment
2022-01-12 08:28:03 -08:00
Leonardo de Moura
b50e82bc93
feat: unfold tactic
2022-01-07 13:51:45 -08:00
Leonardo de Moura
c303bf6916
refactor: add helper methods for simp
2022-01-07 13:51:45 -08:00
Leonardo de Moura
bef161caf7
feat: add better support for discharging equation theorem hypotheses
2022-01-06 14:42:23 -08:00
Leonardo de Moura
90b179bea9
fix: add equation theorems even if definition supports smart unfolding
...
See new test.
2022-01-06 13:53:03 -08:00
Leonardo de Moura
60934bf1d5
feat: add support for removing [simp] attribute from definitions with equational theorems
2022-01-05 16:57:59 -08:00
Leonardo de Moura
c2e52bd577
feat: use getEqnsFor? when applying [simp] at definitions
2022-01-05 15:59:39 -08:00
Leonardo de Moura
030e932db8
feat: use getEqnsFor? at simp
2022-01-05 11:28:24 -08:00
Mario Carneiro
7956a9bb15
chore: typos
2021-12-23 10:14:39 +01:00
Leonardo de Moura
c954fc9ec7
fix: bug at simpLoop
2021-12-18 06:48:08 -08:00
Leonardo de Moura
81f7335269
fix: ensure motive is type correct at simpProj
2021-12-15 17:07:31 -08:00
Leonardo de Moura
0a81093db5
fix: bug at simpProj
...
This bug was reported at https://github.com/dwrensha/lean4-maze/issues/1
2021-12-15 17:07:00 -08:00
Leonardo de Moura
68bd55af32
chore: fix codebase
2021-12-10 13:12:09 -08:00
Leonardo de Moura
96e0e1db98
fix: nontermination at simp [OfNat.ofNat]
...
closes #788
2021-12-10 12:29:33 -08:00
Leonardo de Moura
7b6732a137
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
...
We use the export/extern idiom to define `isLevelDefEqAux`, and then
define the `isDefEq` user facing functions at `Meta/Basic.lean`.
2021-12-06 09:57:00 -08:00
Leonardo de Moura
88b6ad4756
feat: add etaStruct to Meta.Simp.Config
2021-11-25 11:31:00 -08:00
Gabriel Ebner
f55649f81b
fix: prefer simp lemmas with *higher* priority
2021-11-22 11:52:45 -08:00
Leonardo de Moura
2a7b33089a
fix: transparency settings at simp TC check
...
fixes #790
2021-11-15 18:09:31 -08:00
Leonardo de Moura
83cf5b20a1
fix: simpLet
...
Given `let x := v; b`, `simpLet` was using an incorrect local context to simplify `v`.
2021-10-22 16:29:00 -07:00
Leonardo de Moura
b5e640a423
fix: avoid getMVarType' at cleanup tactic
...
`getMVarType'` applies `whnf`
2021-10-19 06:43:07 -07:00
Leonardo de Moura
6b2303b243
fix: bug at tryLemmaCore when numExtraArgs > 1
...
Fixes bug reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Simp.20bug.20-.20produces.60application.20type.20mismatch.60/near/257711901
2021-10-18 13:59:19 -07:00
Sebastian Ullrich
e068833e8d
fix: register missing simp trace classes
2021-10-11 15:37:56 +02:00
Leonardo de Moura
91d2f6d4fc
feat: add cleanup tactic
2021-10-06 19:54:28 -07:00
Leonardo de Moura
59d7b00557
feat: add mapping from mvar user name to MVarId
2021-10-02 15:26:44 -07:00
Leonardo de Moura
dba358067a
chore: remove workaround
2021-09-30 22:37:20 -07:00
Leonardo de Moura
3fed9c9df7
feat: reject partial when if constant is not a function
...
fixes #697
2021-09-28 21:07:14 -07:00
Leonardo de Moura
f1be1d5bba
feat: add simpProj
...
Simplifier for kernel projections.
2021-09-27 19:06:10 -07:00
Leonardo de Moura
2775298fef
feat: add applyMatchSplitter
...
It applies the match splitter without using simplification theorems
2021-09-18 16:30:47 -07:00
Leonardo de Moura
6fbb6c7215
feat: add delta?
2021-09-17 18:46:09 -07:00
Leonardo de Moura
70a4d2691f
chore: cleanup
2021-09-17 16:00:00 -07:00
Leonardo de Moura
42eba87325
feat: add simpMatchTarget
2021-09-17 14:20:28 -07:00
Leonardo de Moura
dc32a827b3
fix: missing instantiateMVars
2021-09-17 14:20:28 -07:00
Leonardo de Moura
35d036b09a
chore: cleanup
2021-09-14 16:09:56 -07:00
Leonardo de Moura
ea37c64b52
feat: add Meta.Rewrite.Config
2021-09-12 18:44:08 -07:00
Leonardo de Moura
54d0fc043e
feat: preserve Expr.mdata at simp
2021-09-11 04:49:36 -07:00
Leonardo de Moura
e667385cf5
feat: simpLet when zeta reduction is disabled
2021-09-10 19:34:38 -07:00
Leonardo de Moura
0cf2c19fc2
fix: condition for selecting split target
...
Only discriminants must not have loose bound variables
2021-09-10 14:56:15 -07:00
Leonardo de Moura
19a710ffc9
feat: add getMatchWithExtra and improve tryLemma at simp
2021-09-09 19:28:09 -07:00
Leonardo de Moura
87f49be5dd
fix: missing withReducible
2021-09-09 18:31:10 -07:00
Leonardo de Moura
496cc92ae9
feat: add simpMatch helper conv tactic
2021-09-09 17:29:32 -07:00
