Mercurial > urweb
comparison lib/ur/list.urs @ 845:6725d73c3c31
Mark current as effectful; add List functions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 09 Jun 2009 11:12:34 -0400 |
parents | 74a1e3bdf430 |
children | 0d30e6338c65 |
comparison
equal
deleted
inserted
replaced
844:74a1e3bdf430 | 845:6725d73c3c31 |
---|---|
1 datatype t = datatype Basis.list | 1 datatype t = datatype Basis.list |
2 | 2 |
3 val show : a ::: Type -> show a -> show (list a) | 3 val show : a ::: Type -> show a -> show (list a) |
4 | |
5 val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b | |
4 | 6 |
5 val rev : a ::: Type -> t a -> t a | 7 val rev : a ::: Type -> t a -> t a |
6 | 8 |
7 val revAppend : a ::: Type -> t a -> t a -> t a | 9 val revAppend : a ::: Type -> t a -> t a -> t a |
8 | 10 |
28 -> (a -> b -> m b) -> b -> t a -> m b | 30 -> (a -> b -> m b) -> b -> t a -> m b |
29 | 31 |
30 val foldlMap : a ::: Type -> b ::: Type -> c ::: Type | 32 val foldlMap : a ::: Type -> b ::: Type -> c ::: Type |
31 -> (a -> b -> c * b) -> b -> t a -> t c * b | 33 -> (a -> b -> c * b) -> b -> t a -> t c * b |
32 | 34 |
33 val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b | |
34 | |
35 val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b | 35 val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b |
36 | 36 |
37 val all : a ::: Type -> (a -> bool) -> t a -> bool | 37 val all : a ::: Type -> (a -> bool) -> t a -> bool |
38 | 38 |
39 val app : m ::: (Type -> Type) -> monad m -> a ::: Type | 39 val app : m ::: (Type -> Type) -> monad m -> a ::: Type |
40 -> (a -> m unit) -> t a -> m unit | 40 -> (a -> m unit) -> t a -> m unit |
41 | |
42 | |
43 (** Association lists *) | |
44 | |
45 val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b | |
46 | |
47 val assocAdd : a ::: Type -> b ::: Type -> eq a -> a -> b -> t (a * b) -> t (a * b) |