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)