summaryrefslogtreecommitdiff
path: root/tests/coq/traits
diff options
context:
space:
mode:
authorRyan Lahfa2024-04-12 20:01:18 +0200
committerRyan Lahfa2024-04-12 20:01:18 +0200
commitc1c33de85906bda71cac098ddba0e5dfc98c85d2 (patch)
tree7feb40276bbfc54e682bbdff2c7db4d287f5a0e4 /tests/coq/traits
parent67eaff0b90d693c86d9848cbf598e7c86caba4c4 (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 'tests/coq/traits')
0 files changed, 0 insertions, 0 deletions