source: src/utilities/lists.ma @ 780

Last change on this file since 780 was 780, checked in by campbell, 9 years ago

Properly update set of registers that are used for pointers in Cminor to
RTLabs phase.

File size: 339 bytes
Line 
1include "basics/list.ma".
2
3let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
4match l with
5[ nil ⇒ None ?
6| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
7].
8
9let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
10match l with
11[ nil ⇒ false
12| cons h t ⇒ orb (p h) (exists A p t)
13].
Note: See TracBrowser for help on using the repository browser.