Idris2Doc : Data.Fin.Lists

Data.Fin.Lists

Functions for collections of `Fin`s

Reexports

import public Data.Fin

rangeFrom0To : Fin n -> List (Fin n): Totality: total
Visibility: public export
rangeFromTo : Fin n -> Fin n -> List (Fin n): Totality: total
Visibility: public export
allGreaterThan : Fin n -> List (Fin n): Totality: total
Visibility: export