|
Last change
on this file since 950 was
816,
checked in by campbell, 10 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 | |
|---|
| 1 | include "basics/list.ma". |
|---|
| 2 | |
|---|
| 3 | let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝ |
|---|
| 4 | match l with |
|---|
| 5 | [ nil ⇒ None ? |
|---|
| 6 | | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ] |
|---|
| 7 | ]. |
|---|
| 8 | |
|---|
| 9 | let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ |
|---|
| 10 | match l with |
|---|
| 11 | [ nil ⇒ False |
|---|
| 12 | | cons h t ⇒ P h ∧ All A P t |
|---|
| 13 | ]. |
|---|
| 14 | |
|---|
| 15 | let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ |
|---|
| 16 | match 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.
