From 69e7653d313773304939de58c575595ece3aa034 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Tue, 23 Apr 2024 16:34:06 +0200 Subject: feat: make `find` a better specification Previously, find := true was matching this spec. It needed to be in PRE/POST style and be an equivalence wrt to the location return value. Alternatively, we import the Order. Signed-off-by: Raito Bezarius --- Verification.lean | 1 + 1 file changed, 1 insertion(+) (limited to 'Verification.lean') diff --git a/Verification.lean b/Verification.lean index 31d8103..4a28407 100644 --- a/Verification.lean +++ b/Verification.lean @@ -1,2 +1,3 @@ import Verification.Insert import Verification.Find +import Verification.Order -- cgit v1.2.3