source: src/ERTL/uses.ma @ 1188

Last change on this file since 1188 was 1188, checked in by mulligan, 9 years ago

removed stray lines from uses.ma so that it at least typechecks

File size: 423 bytes
Line 
1include "ERTL/ERTL.ma".
2
3let rec assoc_list_find
4  (A: Type[0]) (B: Type[0]) (eq_a: A → A → bool) (to_find: A)
5  (def: B) (l: list (A × B))
6    on l ≝
7  match l with
8  [ nil ⇒ def
9  | cons hd tl ⇒
10    if eq_a (\fst hd) to_find then
11      \snd hd
12    else
13      assoc_list_find A B eq_a to_find def tl
14  ].
15     
16definition lookup ≝
17  λuses.
18  λr.
19    assoc_list_find register nat (eq_identifier ?) uses 0 r.
Note: See TracBrowser for help on using the repository browser.