git.iko.soy/Idris-dev
on master help sign in
Merge pull request #136 from DanielWaterworth/useful_functions

Useful functions

commitbc3e8074421a4db007b569f00260e1ed4797a059 authorEdwin Brady <edwin.brady@gmail.com> dateSun 16 Dec 2012, 12:41 (14 years ago) parent28b68fdd087dea
2 files changed+12
compare with master
unifiedsplit
lib/Prelude/Fin.idr+4 lib/Prelude/Vect.idr+8
lib/Prelude/Fin.idr+4
@@ -24,3 +24,7 @@ strengthen {n = S k} (fS i) with (strengthen i)
2424 strengthen (fS k) | Left x = Left (fS x)
2525 strengthen (fS k) | Right x = Right (fS x)
2626strengthen f = Left f
27+
28+last : Fin (S n)
29+last {n=O} = fO
30+last {n=S _} = fS last
lib/Prelude/Vect.idr+8
@@ -301,6 +301,14 @@ catMaybes (Nothing::xs) = catMaybes xs
301301catMaybes ((Just j)::xs) with (catMaybes xs)
302302 | (_ ** tail) = (_ ** j::tail)
303303
304+range : Vect (Fin n) n
305+range =
306+ reverse range_
307+ where
308+ range_ : Vect (Fin n) n
309+ range_ {n=O} = Nil
310+ range_ {n=(S _)} = last :: map weaken range_
311+
304312--------------------------------------------------------------------------------
305313-- Proofs
306314--------------------------------------------------------------------------------