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.8.0-8c970f1ba