Idris2Doc : Libraries.Data.Span

Libraries.Data.Span

(source)
Definitions
record Span : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSpan : Nat -> Nat -> a -> Span a

  Projections:
  
.length : Span a -> Nat
  
.property : Span a -> a
  
.start : Span a -> Nat

  Hints:
  
Foldable Span
  
FromSExpable a => FromSExpable (Span a)
  
Functor Span
  
SExpable a => SExpable (Span a)
  
Show a => Show (Span a)
  
Traversable Span
.start : Span a -> Nat
  Visibility: public export
start : Span a -> Nat
  Visibility: public export
.length : Span a -> Nat
  Visibility: public export
length : Span a -> Nat
  Visibility: public export
.property : Span a -> a
  Visibility: public export
property : Span a -> a
  Visibility: public export