
  0 | ||| Functions for collections of `Fin`s
  1 | module Data.Fin.Lists
  2 | 
  3 | import public Data.Fin
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | rangeFrom0To : Fin n -> List (Fin n)
  9 | rangeFrom0To FZ     = [FZ]
 10 | rangeFrom0To (FS x) = FZ :: (FS <$> rangeFrom0To x)
 11 | 
 12 | public export
 13 | rangeFromTo : Fin n -> Fin n -> List (Fin n)
 14 | rangeFromTo FZ     FZ     = [FZ]
 15 | rangeFromTo FZ     r      = rangeFrom0To r
 16 | rangeFromTo l      FZ     = reverse $ rangeFrom0To l
 17 | rangeFromTo (FS l) (FS r) = FS <$> rangeFromTo l r
 18 | 
 19 | export
 20 | allGreaterThan : {n : _} -> Fin n -> List (Fin n)
 21 | allGreaterThan curr = case strengthen $ FS curr of
 22 |                         Nothing => []
 23 |                         Just next => next :: allGreaterThan (assert_smaller curr next) -- `next` is closer to the upper bound than `curr`
 24 |