Idris2Doc : Libraries.Data.DList

Libraries.Data.DList

(source)
Definitions
record DList : Type -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkDList : (List a -> List a) -> DList a

  Projection: 
.runDList : DList a -> List a -> List a

  Hints:
  
FromString (DList String)
  
Monoid (DList a)
  
Semigroup (DList a)
Nil : DList a
  Totality: total
  Visibility: export
singleton : a -> DList a
  Totality: total
  Visibility: export
(::) : a -> DList a -> DList a
  Totality: total
  Visibility: export
  Fixity Declaration: infixr operator, level 7
snoc : DList a -> a -> DList a
  Totality: total
  Visibility: export
appendR : DList a -> List a -> DList a
  Totality: total
  Visibility: export
appendL : List a -> DList a -> DList a
  Totality: total
  Visibility: export
(++) : DList a -> DList a -> DList a
  Totality: total
  Visibility: export
  Fixity Declaration: infixr operator, level 7
reify : DList a -> List a
  Totality: total
  Visibility: export