Idris2Doc : Data.CheckedEmpty.List.Lazy

Data.CheckedEmpty.List.Lazy

(source)
Reexports
import public Language.Implicits.IfUnsolved
Definitions
data LazyLst : Bool -> Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Nil : LazyLst False a
  
(::) : {auto 0 _ : IfUnsolved True ine} -> {auto 0 _ : IfUnsolved True ne} -> a -> Lazy (LazyLst ine a) -> LazyLst ne a

  Hints:
  
Applicative (LazyLst ne)
  
Biinjective (\x, y => x :: Delay y)
  
Cast (LazyLst ne a) (LazyList a)
  
Foldable (LazyLst ne)
  
Functor (LazyLst ne)
  
Monad (LazyLst ne)
  
Semigroup (LazyLst ne a)
  
Show a => Show (LazyLst ne a)
  
Uninhabited ([] = x :: Delay xs)
  
Uninhabited (x :: Delay xs = [])
  
Either (Uninhabited (x = y)) (Uninhabited (xs = ys)) => Uninhabited (x :: Delay xs = y :: Delay ys)
  
Zippable (LazyLst ne)
LazyLst0 : Type -> Type
  An alias for a list that definitely may be empty.
  Don't use this if you can be polymorphic on the boolean type argument.

  Totality: total
  Visibility: public export
LazyLst1 : Type -> Type
  Totality: total
  Visibility: public export
length : LazyLst ne a -> Nat
  Totality: total
  Visibility: public export
.length : LazyLst ne a -> Nat
  Totality: total
  Visibility: public export
(++) : LazyLst nel a -> Lazy (LazyLst ner a) -> LazyLst (nel || Delay ner) a
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
index' : (xs : LazyLst ne a) -> Fin (xs .length) -> a
  Totality: total
  Visibility: public export
index : Fin n -> (xs : LazyLst ne a) -> {auto 0 _ : n = xs .length} -> a
  Totality: total
  Visibility: public export
iterateN : (n : Nat) -> (a -> a) -> a -> LazyLst (n /= 0) a
  Totality: total
  Visibility: public export
tabulateN : (n : Nat) -> (Fin n -> a) -> LazyLst (n /= 0) a
  Totality: total
  Visibility: public export
replicate : (n : Nat) -> a -> LazyLst (n /= 0) a
  Totality: total
  Visibility: public export
iterate : (a -> Maybe a) -> a -> LazyLst0 a
  Visibility: public export
unfoldr : (b -> Maybe (a, b)) -> b -> LazyLst0 a
  Visibility: public export
relaxF : LazyLst ne a -> LazyLst0 a
  Totality: total
  Visibility: public export
relaxT : LazyLst1 a -> LazyLst ne a
  Totality: total
  Visibility: public export
relaxAnd : LazyLst ne a -> LazyLst (ne && nx) a
  Totality: total
  Visibility: public export
strengthen : LazyLst ne a -> Maybe (LazyLst1 a)
  Totality: total
  Visibility: public export
bind : LazyLst nel a -> (a -> LazyLst ner b) -> LazyLst (nel && Delay ner) b
  Totality: total
  Visibility: public export
bind' : LazyLst nel a -> LazyLst ner b -> LazyLst (nel && Delay ner) b
  Totality: total
  Visibility: public export
join' : LazyLst nel (LazyLst ner a) -> LazyLst (nel && Delay ner) a
  Totality: total
  Visibility: public export
ap : LazyLst nel (a -> b) -> LazyLst ner a -> LazyLst (nel && Delay ner) b
  Totality: total
  Visibility: public export
foldrLazy : (a -> Lazy b -> b) -> Lazy b -> LazyLst ne a -> b
  Totality: total
  Visibility: public export
foldl1 : (a -> a -> a) -> LazyLst1 a -> a
  Totality: total
  Visibility: public export
foldr1 : (a -> Lazy a -> a) -> LazyLst1 a -> a
  Totality: total
  Visibility: public export
traverse_ : Monad m => (a -> m b) -> LazyLst ne a -> m ()
  Totality: total
  Visibility: public export
for_ : Monad m => LazyLst ne a -> (a -> m b) -> m ()
  Totality: total
  Visibility: public export
sequence_ : Monad m => LazyLst ne (m a) -> m ()
  Totality: total
  Visibility: public export
head : LazyLst1 a -> a
  Totality: total
  Visibility: public export
head' : LazyLst ne a -> Maybe a
  Totality: total
  Visibility: public export
tail : LazyLst1 a -> LazyLst0 a
  Totality: total
  Visibility: public export
tail' : LazyLst ne a -> Maybe (LazyLst0 a)
  Totality: total
  Visibility: public export
last : LazyLst1 a -> a
  Totality: total
  Visibility: public export
last' : LazyLst ne a -> Maybe a
  Totality: total
  Visibility: public export
init : LazyLst1 a -> LazyLst0 a
  Totality: total
  Visibility: public export
init' : LazyLst ne a -> Maybe (LazyLst0 a)
  Totality: total
  Visibility: public export
tails : LazyLst ne a -> LazyLst1 (LazyLst0 a)
  Totality: total
  Visibility: public export
tails1 : LazyLst ne a -> LazyLst ne (LazyLst1 a)
  Totality: total
  Visibility: public export
inits : LazyLst ne a -> LazyLst1 (LazyLst0 a)
  Totality: total
  Visibility: public export
inits1 : LazyLst ne a -> LazyLst ne (LazyLst1 a)
  Totality: total
  Visibility: public export
take : (n : Nat) -> LazyLst ne a -> LazyLst (ne && Delay (n /= 0)) a
  Totality: total
  Visibility: public export
drop : Nat -> LazyLst ne a -> LazyLst0 a
  Totality: total
  Visibility: public export
takeWhile : (a -> Bool) -> LazyLst ne a -> LazyLst0 a
  Totality: total
  Visibility: public export
dropWhile : (a -> Bool) -> LazyLst ne a -> LazyLst0 a
  Totality: total
  Visibility: public export
zipWithStream : (a -> b -> c) -> Stream a -> LazyLst ne b -> LazyLst ne c
  Totality: total
  Visibility: public export
zipStream : Stream a -> LazyLst ne b -> LazyLst ne (a, b)
  Totality: total
  Visibility: public export
filter : (a -> Bool) -> LazyLst ne a -> LazyLst0 a
  Totality: total
  Visibility: public export
mapMaybe : (a -> Maybe b) -> LazyLst ne a -> LazyLst0 b
  Totality: total
  Visibility: public export
fromFoldable : Foldable f => f a -> LazyLst0 a
  Totality: total
  Visibility: public export
fromList : (xs : List a) -> LazyLst (not (null xs)) a
  Totality: total
  Visibility: public export
fromLazyList : (xs : LazyList a) -> LazyLst (not (null xs)) a
  Totality: total
  Visibility: public export
toLazyList : LazyLst ne a -> LazyList a
  Totality: total
  Visibility: public export
fromStream : Stream a -> LazyLst1 a
  Visibility: public export
rangeFromTo : Range a => a -> a -> LazyLst0 a
  Totality: total
  Visibility: public export
rangeFromThenTo : Range a => a -> a -> a -> LazyLst0 a
  Totality: total
  Visibility: public export
rangeFrom : Range a => {auto 0 _ : IfUnsolved ne True} -> a -> LazyLst ne a
  Visibility: public export
rangeFromThen : Range a => {auto 0 _ : IfUnsolved ne True} -> a -> a -> LazyLst ne a
  Visibility: public export
mapFusion : (g : (b -> c)) -> (f : (a -> b)) -> (xs : LazyLst ne a) -> map g (map f xs) = map (g . f) xs
  Totality: total
  Visibility: export
mapExt : (xs : LazyLst ne {_:6028}) -> ((x : {_:6028}) -> f x = g x) -> map f xs = map g xs
  Totality: total
  Visibility: export