source: src/utilities/lists.ma @ 956

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

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File size: 471 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 All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
10match l with
11[ nil ⇒ False
12| cons h t ⇒ P h ∧ All A P t
13].
14
15let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
16match l with
17[ nil ⇒ false
18| cons h t ⇒ orb (p h) (exists A p t)
19].
Note: See TracBrowser for help on using the repository browser.