Ignore:
Timestamp:
Nov 30, 2012, 4:40:37 PM (7 years ago)
Author:
garnier
Message:

Some progress on the Cl -> Cm front

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2488 r2510  
    757757     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
    758758] qed.
    759 
    760 (* Lookup functions in list environments (used to type local variables in functions) *)     
    761 let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
    762 match l with
    763 [ nil ⇒ false
    764 | cons hd tl ⇒
    765   let 〈id, ty〉 ≝ hd in
    766   match identifier_eq SymbolTag i id with
    767   [ inl Hid_eq ⇒ true
    768   | inr Hid_neq ⇒ mem_assoc_env i tl 
    769   ]
    770 ].
    771759
    772760(* --------------------------------------------------------------------------- *)
Note: See TracChangeset for help on using the changeset viewer.