diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 5a5f130c..cca52c1d 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -291,6 +291,9 @@ rewrite <- Z.lt_le_pred. auto. Defined. +Definition sint0 {a} `{ArithFact (a >= 0)} (x : mword a) : Z := + if sumbool_of_bool (Z.eqb a 0) then 0 else projT1 (sint x). + Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0. unfold length_list. auto with zarith. |