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

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

File size:
423 bytes

Line  

1  include "ERTL/ERTL.ma". 

2  

3  let 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  

16  definition 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.