Changeset 15 for C-semantics/Integers.ma


Ignore:
Timestamp:
Jul 22, 2010, 4:50:06 PM (9 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r14 r15  
    156156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
    157157
     158(*
    158159ndefinition zero_ext : Z → int → int ≝
    159160λn,x. repr (modZ (unsigned x) (two_p n)).
    160161ndefinition sign_ext : Z → int → int ≝
    161162λ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*)
     166nlet rec zero_ext (n:Z) (x:int) on x : int ≝
     167  repr (modZ (unsigned x) (two_p n)).
     168nlet rec sign_ext (n:Z) (x:int) on x : int ≝
     169  repr (let p ≝ two_p n in
    162170        let y ≝ modZ (unsigned x) p in
    163171        if Zltb y (two_p (n-1)) then y else y - p).
Note: See TracChangeset for help on using the changeset viewer.