Changeset 15 for C-semantics/Integers.ma
- Timestamp:
- Jul 22, 2010, 4:50:06 PM (11 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/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 (n-1)) 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 (n-1)) then y else y - p).
Note: See TracChangeset
for help on using the changeset viewer.