diff options
| author | Raito Bezarius | 2024-04-23 16:34:06 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-23 16:34:55 +0200 |
| commit | 69e7653d313773304939de58c575595ece3aa034 (patch) | |
| tree | c949a7274e113246816bb07110d02a2abb9d85a9 /Verification.lean | |
| parent | d3ea366adcd71d0ef15ffbc5d35ca998aa53f19a (diff) | |
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 <masterancpp@gmail.com>
Diffstat (limited to '')
| -rw-r--r-- | Verification.lean | 1 |
1 files changed, 1 insertions, 0 deletions
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 |