Ignore:
Timestamp:
Jan 25, 2011, 5:30:36 PM (9 years ago)
Author:
campbell
Message:

Prevent clashes between names in AST and other parts of the development.
(Noticed when trying a large example file.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/AST.ma

    r467 r478  
    5555
    5656ninductive typ : Type ≝
    57   | Tint : typ
    58   | Tfloat : typ.
     57  | ASTint : typ
     58  | ASTfloat : typ.
    5959
    6060ndefinition typesize : typ → Z ≝ λty.
    61   match ty return λ_.Z with  [ Tint ⇒ 4 | Tfloat ⇒ 8 ].
     61  match ty return λ_.Z with  [ ASTint ⇒ 4 | ASTfloat ⇒ 8 ].
    6262
    6363nlemma typesize_pos: ∀ty. typesize ty > 0.
     
    8787ndefinition proj_sig_res : signature → typ ≝ λs.
    8888  match sig_res s with
    89   [ None ⇒ Tint
     89  [ None ⇒ ASTint
    9090  | Some t ⇒ t
    9191  ].
     
    415415  ef_sig: signature
    416416}.
    417 
     417(*
    418418ninductive fundef (F: Type): Type ≝
    419419  | Internal: F → fundef F
     
    433433  | External ef ⇒ External ? ef
    434434  ].
    435 
     435*)
    436436(*
    437437End TRANSF_FUNDEF.
Note: See TracChangeset for help on using the changeset viewer.