diff options
| author | Son Ho | 2023-07-25 16:26:08 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-25 16:26:08 +0200 |
| commit | 1854c631a6a7a3f8d45ad18e05547f9d3782c3ee (patch) | |
| tree | 270e16d5c106d00b0e18520bf89d05d1e202cdb6 /backends/lean/Base/Arith/Int.lean | |
| parent | 876137dff361620d8ade1a4ee94fa9274df0bdc6 (diff) | |
Make progress on the hashmap properties
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 3415866e..bc0676d8 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -225,6 +225,8 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess : Tactic.TacticM Unit) : Ta -- Preprocess - wondering if we should do this before or after splitting -- the goal. I think before leads to a smaller proof term? Tactic.allGoals (intTacPreprocess extraPreprocess) + -- More preprocessing + Tactic.allGoals (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard) -- Split the conjunctions in the goal if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget) -- Call linarith |