michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/bv): Add signed/unsigned comparisons.

Browse source
This commit is contained in:
Joe Hendrix 2015-11-30 07:40:20 -08:00 committed by Leonardo de Moura
parent 5cf6e18af0
commit fd1999a97f
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/data/bv.lean
View file

@ -128,6 +128,22 @@ section arith
definition bv_has_neg [instance] : has_neg (bv n) := has_neg.mk bv_neg
definition bv_has_mul [instance] : has_mul (bv n) := has_mul.mk bv_mul
definition bv_ult : bv n → bv n → bool := λx y, pr₁ (bv_sbb x y ff)
definition bv_ugt : bv n → bv n → bool := λx y, bv_ult y x
definition bv_ule : bv n → bv n → bool := λx y, bnot (bv_ult y x)
definition bv_uge : bv n → bv n → bool := λx y, bv_ule y x
definition bv_slt : bv (succ n) → bv (succ n) → bool := λx y,
cond (head x)
(cond (head y)
(bv_ult (tail x) (tail y)) -- both negative
tt) -- x is negative and y is not
(cond (head y)
ff -- y is negative and x is not
(bv_ult (tail x) (tail y))) -- both positive
definition bv_sgt : bv (succ n) → bv (succ n) → bool := λx y, bv_slt y x
definition bv_sle : bv (succ n) → bv (succ n) → bool := λx y, bnot (bv_slt y x)
definition bv_sge : bv (succ n) → bv (succ n) → bool := λx y, bv_sle y x
end arith