Added a function, 'range', that returns all of the elements of a finite set, in order, in a vector
commitd087dea80789b0166cac5e8c5b3f60fb54bf682a
authorDaniel Waterworth <Da.Waterworth@gmail.com>
dateSun 16 Dec 2012, 14:33 (14 years ago)
parent34392c9
lib/Prelude/Vect.idr+8
@@ -288,6 +288,14 @@ catMaybes (Nothing::xs) = catMaybes xs
288288catMaybes ((Just j)::xs) with (catMaybes xs)
289289 | (_ ** tail) = (_ ** j::tail)
290290
291+range : Vect (Fin n) n
292+range =
293+ reverse range_
294+ where
295+ range_ : Vect (Fin n) n
296+ range_ {n=O} = Nil
297+ range_ {n=(S _)} = last :: map weaken range_
298+
291299--------------------------------------------------------------------------------
292300-- Proofs
293301--------------------------------------------------------------------------------