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)