source: src/utilities/lists.ma @ 778

Last change on this file since 778 was 766, checked in by campbell, 10 years ago

Most of the Cminor to RTLabs stage.

Is buggy, generates inefficient RTLabs in a couple of places and is missing
St_switch.

File size: 198 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].
Note: See TracBrowser for help on using the repository browser.