git.iko.soy/Idris-dev
on master help sign in
Added a function, 'range', that returns all of the elements of a finite set, in order, in a vector
d087deaDaniel Waterworth
lib/Prelude/Vect.idr+8
compare with master
unifiedsplit
@@ -288,6 +288,14 @@ catMaybes (Nothing::xs) = catMaybes xs
288catMaybes ((Just j)::xs) with (catMaybes xs)
288catMaybes ((Just j)::xs) with (catMaybes xs)
289 | (_ ** tail) = (_ ** j::tail)
289 | (_ ** tail) = (_ ** j::tail)
290
290
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+
291--------------------------------------------------------------------------------
299--------------------------------------------------------------------------------
292-- Proofs
300-- Proofs
293--------------------------------------------------------------------------------
301--------------------------------------------------------------------------------