
Meta-data
- Description: Linked Lists
- Authors: Dominic Orchard, Vilem-Benjamin Liepelt
- License: BSD3
- Copyright: (c) Authors 2018
- Issue-tracking: https://github.com/dorchard/granule/issues
- Repository: https://github.com/dorchard/granule
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)