Ignore:
Timestamp:
Jan 15, 2013, 3:58:12 PM (7 years ago)
Author:
garnier
Message:

Some progress on CL to CM.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2578 r2582  
    673673
    674674axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
     675
     676(* dividing zero by something eq zero, not the other way around ofc. *)
     677axiom division_u_zero : ∀sz.∀v:BitVector ?. division_u sz (bv_zero ?) v = Some ? (bv_zero ?).
     678
    675679
    676680(* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *)
Note: See TracChangeset for help on using the changeset viewer.