Changeset 11 for C-semantics/extralib.ma


Ignore:
Timestamp:
Jul 7, 2010, 12:55:01 PM (10 years ago)
Author:
campbell
Message:

Fill in some axioms to aid executablity.
Implement global variable lookups and funtion returns.
Update compcert patch to use binary representation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/extralib.ma

    r10 r11  
    267267##] nqed.
    268268
    269 naxiom Z_times : Z → Z → Z.
     269ndefinition Z_times : Z → Z → Z ≝
     270λx,y. match x with
     271[ OZ ⇒ OZ
     272| pos n ⇒
     273  match y with
     274  [ OZ ⇒ OZ
     275  | pos m ⇒ pos (n*m)
     276  | neg m ⇒ neg (n*m)
     277  ]
     278| neg n ⇒
     279  match y with
     280  [ OZ ⇒ OZ
     281  | pos m ⇒ neg (n*m)
     282  | neg m ⇒ pos (n*m)
     283  ]
     284].
    270285interpretation "integer multiplication" 'times x y = (Z_times x y).
    271286
Note: See TracChangeset for help on using the changeset viewer.