Changeset 961 for src/common/Events.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/Events.ma

    r879 r961  
    3737  world. *)
    3838
    39 inductive eventval: Type[0] :=
    40   | EVint: int -> eventval
    41   | EVfloat: float -> eventval.
     39inductive eventval: Type[0]
     40  | EVint: ∀sz. bvint sz → eventval
     41  | EVfloat: float eventval.
    4242
    4343inductive event : Type[0] ≝
     
    193193inductive eventval_match: eventval -> typ -> val -> Prop :=
    194194  | ev_match_int:
    195       ∀i,sz,sg. eventval_match (EVint i) (ASTint sz sg) (Vint i)
     195      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
    196196  | ev_match_float:
    197197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
Note: See TracChangeset for help on using the changeset viewer.