summaryrefslogtreecommitdiff
path: root/AvlVerification.lean
diff options
context:
space:
mode:
authorRaito Bezarius2024-04-23 16:34:06 +0200
committerRaito Bezarius2024-04-23 16:34:55 +0200
commit69e7653d313773304939de58c575595ece3aa034 (patch)
treec949a7274e113246816bb07110d02a2abb9d85a9 /AvlVerification.lean
parentd3ea366adcd71d0ef15ffbc5d35ca998aa53f19a (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 '')
0 files changed, 0 insertions, 0 deletions