Changeset 961 for src/common/Floats.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Floats.ma

    r700 r961  
    3434axiom Fabs: float → float.
    3535axiom singleoffloat: float → float.
    36 axiom intoffloat: float → int.
    37 axiom intuoffloat: float → int.
    38 axiom floatofint: int → float.
    39 axiom floatofintu: int → float.
     36axiom intoffloat: ∀n. float → BitVector n.
     37axiom intuoffloat: ∀n. float → BitVector n.
     38axiom floatofint: ∀n. BitVector n → float.
     39axiom floatofintu: ∀n. BitVector n → float.
    4040
    4141axiom Fadd: float → float → float.
Note: See TracChangeset for help on using the changeset viewer.