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/Tree.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 'Verification/Tree.lean')
0 files changed, 0 insertions, 0 deletions