Changeset 2468 for src/common/Events.ma
- Timestamp:
- Nov 15, 2012, 6:12:57 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Events.ma
r1599 r2468 38 38 39 39 inductive eventval: Type[0] ≝ 40 | EVint: ∀sz. bvint sz → eventval 41 | EVfloat: float → eventval. 40 | EVint: ∀sz. bvint sz → eventval. 41 (* | EVfloat: float → eventval.*) 42 42 43 43 inductive event : Type[0] ≝ … … 194 194 | ev_match_int: 195 195 ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i) 196 | ev_match_float:197 ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f) .196 (* | ev_match_float: 197 ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f) *). 198 198 199 199 inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
Note: See TracChangeset
for help on using the changeset viewer.