Changeset 15 for Csemantics/Integers.ma
 Timestamp:
 Jul 22, 2010, 4:50:06 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Integers.ma
r14 r15 156 156 ndefinition neg : int → int ≝ λx. repr ( unsigned x). 157 157 158 (* 158 159 ndefinition zero_ext : Z → int → int ≝ 159 160 λn,x. repr (modZ (unsigned x) (two_p n)). 160 161 ndefinition sign_ext : Z → int → int ≝ 161 162 λn,x. repr (let p ≝ two_p n in 163 let y ≝ modZ (unsigned x) p in 164 if Zltb y (two_p (n1)) then y else y  p). 165 *) 166 nlet rec zero_ext (n:Z) (x:int) on x : int ≝ 167 repr (modZ (unsigned x) (two_p n)). 168 nlet rec sign_ext (n:Z) (x:int) on x : int ≝ 169 repr (let p ≝ two_p n in 162 170 let y ≝ modZ (unsigned x) p in 163 171 if Zltb y (two_p (n1)) then y else y  p).
Note: See TracChangeset
for help on using the changeset viewer.