summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith
diff options
context:
space:
mode:
authorSon Ho2023-07-25 19:06:05 +0200
committerSon Ho2023-07-25 19:06:05 +0200
commit0cc3c78137434d848188eee2a66b1e2cacfd102e (patch)
tree43c9cee6a846f634ecd9f144c3c3f51934c7f81e /backends/lean/Base/Arith
parent1854c631a6a7a3f8d45ad18e05547f9d3782c3ee (diff)
Make progress on the proofs of the hashmap
Diffstat (limited to 'backends/lean/Base/Arith')
-rw-r--r--backends/lean/Base/Arith/Int.lean1
1 files changed, 1 insertions, 0 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index bc0676d8..48a30a49 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -43,6 +43,7 @@ instance (x y : Int) : IsLinearIntProp (x > y) where
instance (x y : Int) : IsLinearIntProp (x ≤ y) where
instance (x y : Int) : IsLinearIntProp (x ≥ y) where
instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+instance (x y : Int) : IsLinearIntProp (x = y) where
/- It seems we don't need to do any special preprocessing when the *goal*
has the following shape - I guess `linarith` automatically calls `intro` -/
instance (x y : Int) : IsLinearIntProp (¬ x = y) where