Changeset 1878 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Apr 4, 2012, 6:48:27 PM (8 years ago)
Author:
campbell
Message:

Enforce typing of constants in front-end, plus binops for RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r1872 r1878  
    44include "basics/lists/list.ma".
    55
    6 (* TODO: consider making the typing stricter. *)
    7 
    86inductive expr : typ → Type[0] ≝
    97| Id : ∀t. ident → expr t
    10 | Cst : ∀t. constant → expr t
     8| Cst : ∀t. constant t → expr t
    119| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    1210| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
Note: See TracChangeset for help on using the changeset viewer.