From 0cc3c78137434d848188eee2a66b1e2cacfd102e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jul 2023 19:06:05 +0200 Subject: Make progress on the proofs of the hashmap --- backends/lean/Base/Arith/Int.lean | 1 + 1 file changed, 1 insertion(+) (limited to 'backends/lean/Base/Arith') 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 -- cgit v1.2.3