diff options
| author | Son HO | 2024-06-22 13:22:32 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-22 13:22:32 +0200 |
| commit | 8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c (patch) | |
| tree | b3de971e89c369f30de349806c87913edeb17333 /backends/lean/Base/Arith/Scalar.lean | |
| parent | 4d30546c809cb2c512e0c3fd8ee540fff1330eab (diff) | |
Improve `scalar_tac` and `scalar_decr_tac` (#256)
* Fix an issue in a proof of the hashmap
* Improve scalar_decr_tac
* Improve the error message of scalar_tac and add the missing Termination.lean
Diffstat (limited to 'backends/lean/Base/Arith/Scalar.lean')
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 31110b95..a36aadf3 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -44,17 +44,6 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do elab "scalar_tac" : tactic => scalarTac false --- For termination proofs -syntax "scalar_decr_tac" : tactic -macro_rules - | `(tactic| scalar_decr_tac) => - `(tactic| - simp_wf; - -- TODO: don't use a macro (namespace problems) - (first | apply Arith.to_int_to_nat_lt - | apply Arith.to_int_sub_to_nat_lt) <;> - simp_all <;> scalar_tac) - instance (ty : ScalarTy) : HasIntProp (Scalar ty) where -- prop_ty is inferred prop := λ x => And.intro x.hmin x.hmax |