Changeset 15 for C-semantics/Integers.ma

Timestamp:

Jul 22, 2010, 4:50:06 PM (11 years ago)

Author:

campbell

Message:

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File:

• C-semantics/Integers.ma (modified) (1 diff)

C-semantics/Integers.ma

@@ -156 +156 @@
 ndefinition neg : int → int ≝ λx. repr (- unsigned x).
 
+(*
 ndefinition zero_ext : Z → int → int ≝
 λn,x. repr (modZ (unsigned x) (two_p n)).
 ndefinition sign_ext : Z → int → int ≝
 λn,x. repr (let p ≝ two_p n in
+        let y ≝ modZ (unsigned x) p in
+        if Zltb y (two_p (n-1)) then y else y - p).
+*)
+nlet rec zero_ext (n:Z) (x:int) on x : int ≝
+  repr (modZ (unsigned x) (two_p n)).
+nlet rec sign_ext (n:Z) (x:int) on x : int ≝
+  repr (let p ≝ two_p n in
         let y ≝ modZ (unsigned x) p in
         if Zltb y (two_p (n-1)) then y else y - p).