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