The Index type family is used throughout the library to point into sequences, in may cases with an Integral constraint (e.g., take and drop). It would be useful to have a length function that gave the length of a sequence as Index seq.
This is my current workaround, which should be correct in all cases:
The
Index
type family is used throughout the library to point into sequences, in may cases with anIntegral
constraint (e.g.,take
anddrop
). It would be useful to have a length function that gave the length of a sequence asIndex seq
.This is my current workaround, which should be correct in all cases: