equal
deleted
inserted
replaced
|
1 (* Title: ZF/UNITY/ListPlus.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 More about lists |
|
7 |
|
8 *) |
|
9 |
|
10 ListPlus = NatPlus + |
|
11 |
|
12 constdefs |
|
13 (* Function `take' returns the first n elements of a list *) |
|
14 take :: [i,i]=>i |
|
15 "take(n, as) == list_rec(lam n:nat. [], |
|
16 %a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n" |
|
17 |
|
18 (* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *) |
|
19 |
|
20 nth :: [i, i]=>i |
|
21 "nth(n, as) == list_rec(lam n:nat. 0, |
|
22 %a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n" |
|
23 |
|
24 end |