Changeset 2510 for src/Clight/switchRemoval.ma
- Timestamp:
- Nov 30, 2012, 4:40:37 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2488 r2510 757 757 <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl 758 758 ] 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 with763 [ nil ⇒ false764 | cons hd tl ⇒765 let 〈id, ty〉 ≝ hd in766 match identifier_eq SymbolTag i id with767 [ inl Hid_eq ⇒ true768 | inr Hid_neq ⇒ mem_assoc_env i tl769 ]770 ].771 759 772 760 (* --------------------------------------------------------------------------- *)
Note: See TracChangeset
for help on using the changeset viewer.