Idris2Doc : Data.Seq.Internal
Index
Default
Alternative
Black & White
Definitions data Elem : Type -> Type
Totality : total Visibility : public export Constructor : MkElem : a -> Elem a
Hints : Applicative Elem
Eq a => Eq (Elem a )
Functor Elem
Ord a => Ord (Elem a )
Show a => Show (Elem a )
Sized (Elem a )
unElem : Elem a -> a
Totality : total Visibility : export data FingerTree : Type -> Type
Totality : total Visibility : public export Constructors : Empty : FingerTree e
Single : e -> FingerTree e
Deep : Nat -> Digit e -> FingerTree (Node e ) -> Digit e -> FingerTree e
Hints : Sized a => Eq a => Eq (FingerTree a )
Foldable FingerTree
Functor FingerTree
Sized a => Ord a => Ord (FingerTree a )
Show a => Show (FingerTree a )
Sized e => Sized (FingerTree e )
Traversable FingerTree
reverseTree : (a -> a ) -> FingerTree a -> FingerTree a
Totality : total Visibility : export lookupTree : Sized a => Nat -> FingerTree a -> (Nat , a )
Totality : total Visibility : export adjustTree : Sized a => (Nat -> a -> a ) -> Nat -> FingerTree a -> FingerTree a
Totality : total Visibility : export viewLTree : Sized a => FingerTree a -> Maybe (a , FingerTree a )
Totality : total Visibility : export viewRTree : Sized a => FingerTree a -> Maybe (FingerTree a , a )
Totality : total Visibility : export consTree : Sized e => e -> FingerTree e -> FingerTree e
Totality : total Visibility : export Fixity Declaration : infixr operator, level 5 snocTree : Sized e => FingerTree e -> e -> FingerTree e
Totality : total Visibility : export Fixity Declaration : infixl operator, level 5 split : Nat -> FingerTree (Elem a ) -> (FingerTree (Elem a ), FingerTree (Elem a ))
Totality : total Visibility : export addTree0 : FingerTree (Elem a ) -> FingerTree (Elem a ) -> FingerTree (Elem a )
Totality : total Visibility : export toList' : FingerTree (Elem a ) -> List a
Totality : total Visibility : export replicate' : Nat -> e -> FingerTree (Elem e )
Totality : total Visibility : export length' : FingerTree (Elem e ) -> Nat
Totality : total Visibility : export zipWith' : (a -> b -> c ) -> FingerTree (Elem a ) -> FingerTree (Elem b ) -> FingerTree (Elem c )
Totality : total Visibility : export zipWith3' : (a -> b -> c -> d ) -> FingerTree (Elem a ) -> FingerTree (Elem b ) -> FingerTree (Elem c ) -> FingerTree (Elem d )
Totality : total Visibility : export unzipWith' : (a -> (b , c )) -> FingerTree (Elem a ) -> (FingerTree (Elem b ), FingerTree (Elem c ))
Totality : total Visibility : export unzipWith3' : (a -> (b , (c , d ))) -> FingerTree (Elem a ) -> (FingerTree (Elem b ), (FingerTree (Elem c ), FingerTree (Elem d )))
Totality : total Visibility : export Produced by Idris 2 version 0.7.0