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/frontend_misc.ma

    r2500 r2510  
    285285(* General results on lists. *)
    286286(* --------------------------------------------------------------------------- *)
     287
     288let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
     289match l with
     290[ nil ⇒ false
     291| cons hd tl ⇒
     292  let 〈id, ty〉 ≝ hd in
     293  match identifier_eq SymbolTag i id with
     294  [ inl Hid_eq ⇒ true
     295  | inr Hid_neq ⇒ mem_assoc_env i tl 
     296  ]
     297].
    287298
    288299(* If mem succeeds in finding an element, then the list can be partitioned around this element. *)
Note: See TracChangeset for help on using the changeset viewer.