Changeset 1207 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Sep 12, 2011, 4:20:57 PM (8 years ago)
Author:
campbell
Message:

Second part of fixing temporaries in Clight to Cminor stage.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r961 r1207  
    319319alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
    320320
     321definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
     322definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
     323definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
     324definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
     325
    321326definition bitvector_of_bool:
    322327      ∀n: nat. ∀b: bool. BitVector (S n) ≝
Note: See TracChangeset for help on using the changeset viewer.