
  0 | -- This ought to go into base at some future point
  1 | module Libraries.Data.Span
  2 | 
  3 | public export
  4 | record Span (a : Type) where
  5 |   constructor MkSpan
  6 |   start    : Nat
  7 |   length   : Nat
  8 |   property : a
  9 | 
 10 | export
 11 | Functor Span where
 12 |   map f = { property $= f }
 13 | 
 14 | export
 15 | Foldable Span where
 16 |   foldr c n span = c span.property n
 17 | 
 18 | export
 19 | Traversable Span where
 20 |   traverse f (MkSpan start width prop)
 21 |     = MkSpan start width <$> f prop
 22 | 
 23 | export
 24 | Show a => Show (Span a) where
 25 |   show (MkSpan start width prop)
 26 |     = concat {t = List} [ "[", show start, "-", show width, "]"
 27 |                         , show prop
 28 |                         ]
 29 |