git.iko.soy/Idris-dev
on master help sign in
Merge pull request #136 from DanielWaterworth/useful_functions
bc3e807Edwin Brady
lib/Prelude/Fin.idr+4
compare with master
unifiedsplit
@@ -24,3 +24,7 @@ strengthen {n = S k} (fS i) with (strengthen i)
24 strengthen (fS k) | Left x = Left (fS x)
24 strengthen (fS k) | Left x = Left (fS x)
25 strengthen (fS k) | Right x = Right (fS x)
25 strengthen (fS k) | Right x = Right (fS x)
26strengthen f = Left f
26strengthen 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
301catMaybes ((Just j)::xs) with (catMaybes xs)
301catMaybes ((Just j)::xs) with (catMaybes xs)
302 | (_ ** tail) = (_ ** j::tail)
302 | (_ ** tail) = (_ ** j::tail)
303
303
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+
304--------------------------------------------------------------------------------
312--------------------------------------------------------------------------------
305-- Proofs
313-- Proofs
306--------------------------------------------------------------------------------
314--------------------------------------------------------------------------------