Module List

Meta-data

Contents

data List (a : Type) where
    Empty 
  ; Next a (List a)

append_list : forall {a : Type} 
            . (List a) -> (List a) -> List a
Append two lists
singleton_list : forall {a : Type} 
               . a -> List a
Make a singleton list
length_list : forall {a : Type} 
            . (List (a [0])) -> Int
Length function must ignore the elements
lmap : forall {a : Type, b : Type} 
     . ((a -> b) [0..∞]) -> (List a) -> List b
Map function for lists
lookupBy : forall {a : Type, b : Type} 
         . ((a -> a -> Bool) [0..∞]) -> (a [0..∞]) -> ((List (a, b)) [0..1]) -> Maybe b
Lookup function
head_list : forall {a : Type} 
          . ((List a) [0..1]) -> Result a
Safe head function
foldr_list : forall {a : Type, b : Type} 
           . ((a -> b -> b) [0..∞]) -> b -> (List a) -> b
Foldr on lists
pushList : forall {s : Coeffect, r : s, a : Type} 
         . {((1 : s)) ≤ r, Pushable r} =>
    ((List a) [r]) -> List (a [r])
Push a graded modality inside a list (defined as push @List)
pullList : forall {s : Coeffect, r : s, a : Type} 
         . (List (a [r])) -> (List a) [r]
Pull a graded modality out of a list (defined as pull @List)
return_list : forall {a : Type} 
            . a -> List a

bind_list : forall {a : Type, b : Type} 
          . ((a -> List b) [(0 : Ext Nat)..∞]) -> (List a) -> List b

join_list : forall {a : Type} 
          . (List (List a)) -> List a