diff options
| author | Son Ho | 2023-09-18 12:25:40 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-18 12:25:40 +0200 |
| commit | 1fc263ec0f527698b2f4d734d9757c9f723d0bee (patch) | |
| tree | 5ad211f79e598a96dd9e867289fc601a2f7e2815 /backends/lean/Base/Arith/Int.lean | |
| parent | 888565dd83636522564c6fcae1571735b32125da (diff) | |
Improve scalar_tac
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index eb6701c2..3359ecdb 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -211,9 +211,11 @@ def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM U let _ ← introHasIntPropInstances -- Extra preprocessing, before we split on the disjunctions extraPreprocess - -- Split - let asms ← introInstances ``PropHasImp.concl lookupPropHasImp - splitOnAsms asms.toList + -- Split - note that the extra-preprocessing step might actually have + -- proven the goal (by doing simplifications for instance) + Tactic.allGoals do + let asms ← introInstances ``PropHasImp.concl lookupPropHasImp + splitOnAsms asms.toList elab "int_tac_preprocess" : tactic => intTacPreprocess (do pure ()) |