Idris2Doc : Data.CheckedEmpty.List

Data.CheckedEmpty.List

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

  Hints:
  
Applicative (Lst ne)
  
Biinjective (::)
  
Cast (List1 a) (Lst True a)
  
Cast (Lst True a) (List1 a)
  
Cast (Vect n a) (Lst (n /= 0) a)
  
Foldable (Lst ne)
  
Functor (Lst ne)
  
Monad (Lst ne)
  
Semigroup (Lst ne a)
  
Show a => Show (Lst ne a)
  
Traversable (Lst ne)
  
Uninhabited ([] = x :: xs)
  
Uninhabited (x :: xs = [])
  
Either (Uninhabited (x = y)) (Uninhabited (xs = ys)) => Uninhabited (x :: xs = y :: ys)
  
Zippable (Lst ne)
Lst0 : 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
Lst1 : Type -> Type
  Totality: total
  Visibility: public export
length : Lst ne a -> Nat
  Totality: total
  Visibility: public export
.length : Lst ne a -> Nat
  Totality: total
  Visibility: public export
(++) : Lst nel a -> Lst ner a -> Lst (nel || Delay ner) a
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
index' : (xs : Lst ne a) -> Fin (xs .length) -> a
  Totality: total
  Visibility: public export
index : Fin n -> (xs : Lst ne a) -> {auto 0 _ : n = xs .length} -> a
  Totality: total
  Visibility: public export
iterateN : (n : Nat) -> (a -> a) -> a -> Lst (n /= 0) a
  Totality: total
  Visibility: public export
tabulateN : (n : Nat) -> (Fin n -> a) -> Lst (n /= 0) a
  Totality: total
  Visibility: public export
replicate : (n : Nat) -> a -> Lst (n /= 0) a
  Totality: total
  Visibility: public export
iterate : (a -> Maybe a) -> a -> Lst0 a
  Visibility: public export
unfoldr : (b -> Maybe (a, b)) -> b -> Lst0 a
  Visibility: public export
relaxF : Lst ne a -> Lst0 a
  Totality: total
  Visibility: public export
relaxT : Lst1 a -> Lst ne a
  Totality: total
  Visibility: public export
relaxAnd : Lst ne a -> Lst (ne && nx) a
  Totality: total
  Visibility: public export
strengthen : Lst ne a -> Maybe (Lst1 a)
  Totality: total
  Visibility: public export
bind : Lst nel a -> (a -> Lst ner b) -> Lst (nel && Delay ner) b
  Totality: total
  Visibility: public export
bind' : Lst nel a -> Lst ner b -> Lst (nel && Delay ner) b
  Totality: total
  Visibility: public export
join' : Lst nel (Lst ner a) -> Lst (nel && Delay ner) a
  Totality: total
  Visibility: public export
ap : Lst nel (a -> b) -> Lst ner a -> Lst (nel && Delay ner) b
  Totality: total
  Visibility: public export
foldrLazy : (a -> Lazy b -> b) -> Lazy b -> Lst ne a -> b
  Totality: total
  Visibility: public export
foldl1 : (a -> a -> a) -> Lst1 a -> a
  Totality: total
  Visibility: public export
foldr1 : (a -> Lazy a -> a) -> Lst1 a -> a
  Totality: total
  Visibility: public export
reverse : Lst ne a -> Lst ne a
  Totality: total
  Visibility: public export
head : Lst1 a -> a
  Totality: total
  Visibility: public export
head' : Lst ne a -> Maybe a
  Totality: total
  Visibility: public export
tail : Lst1 a -> Lst0 a
  Totality: total
  Visibility: public export
tail' : Lst ne a -> Maybe (Lst0 a)
  Totality: total
  Visibility: public export
last : Lst1 a -> a
  Totality: total
  Visibility: public export
last' : Lst ne a -> Maybe a
  Totality: total
  Visibility: public export
init : Lst1 a -> Lst0 a
  Totality: total
  Visibility: public export
init' : Lst ne a -> Maybe (Lst0 a)
  Totality: total
  Visibility: public export
unsnoc : Lst1 a -> (Lst0 a, a)
  Totality: total
  Visibility: public export
tails : Lst ne a -> Lst1 (Lst0 a)
  Totality: total
  Visibility: public export
tails1 : Lst ne a -> Lst ne (Lst1 a)
  Totality: total
  Visibility: public export
inits : Lst ne a -> Lst1 (Lst0 a)
  Totality: total
  Visibility: public export
inits1 : Lst ne a -> Lst ne (Lst1 a)
  Totality: total
  Visibility: public export
take : (n : Nat) -> Lst ne a -> Lst (ne && Delay (n /= 0)) a
  Totality: total
  Visibility: public export
drop : Nat -> Lst ne a -> Lst0 a
  Totality: total
  Visibility: public export
takeWhile : (a -> Bool) -> Lst ne a -> Lst0 a
  Totality: total
  Visibility: public export
dropWhile : (a -> Bool) -> Lst ne a -> Lst0 a
  Totality: total
  Visibility: public export
zipWithStream : (a -> b -> c) -> Stream a -> Lst ne b -> Lst ne c
  Totality: total
  Visibility: public export
zipStream : Stream a -> Lst ne b -> Lst ne (a, b)
  Totality: total
  Visibility: public export
filter : (a -> Bool) -> Lst ne a -> Lst0 a
  Totality: total
  Visibility: public export
mapMaybe : (a -> Maybe b) -> Lst ne a -> Lst0 b
  Totality: total
  Visibility: public export
fromFoldable : Foldable f => f a -> Lst0 a
  Totality: total
  Visibility: public export
fromList : (xs : List a) -> Lst (not (null xs)) a
  Totality: total
  Visibility: public export
fromList1 : List1 a -> Lst1 a
  Totality: total
  Visibility: public export
toList1 : Lst1 a -> List1 a
  Totality: total
  Visibility: public export
fromVect : Vect n a -> Lst (n /= 0) a
  Totality: total
  Visibility: public export
rangeFromTo : Range a => a -> a -> Lst0 a
  Totality: total
  Visibility: public export
rangeFromThenTo : Range a => a -> a -> a -> Lst0 a
  Totality: total
  Visibility: public export
mapFusion : (g : (b -> c)) -> (f : (a -> b)) -> (xs : Lst ne a) -> map g (map f xs) = map (g . f) xs
  Totality: total
  Visibility: export
mapExt : (xs : Lst ne {_:6143}) -> ((x : {_:6143}) -> f x = g x) -> map f xs = map g xs
  Totality: total
  Visibility: export