diff options
| author | Ryan Lahfa | 2024-04-12 20:01:18 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-04-12 20:01:18 +0200 |
| commit | c1c33de85906bda71cac098ddba0e5dfc98c85d2 (patch) | |
| tree | 7feb40276bbfc54e682bbdff2c7db4d287f5a0e4 /tests/hol4/misc-loops | |
| parent | 67eaff0b90d693c86d9848cbf598e7c86caba4c4 (diff) | |
lean: scalars form a preorder
Via the canonical injection, we can easily define an induced preorder on
scalars and inherit all nice properties.
It's useful to reason on specific scalar preorders w.r.t. Ordering, see
the binary search tree verification example.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions