Merge pull request #425 from Melvar/simplify-range
Simplify Prelude.Vect.range
commit86914e3520172195480f84e6849673550e8215ea
authorEdwin Brady <edwin.brady@gmail.com>
dateSun 28 Jul 2013, 11:56 (13 years ago)
parentbf8cfc58bc1c7f
lib/Prelude/Vect.idr+2−6
@@ -323,12 +323,8 @@ diag [] = []
323323diag ((x::xs)::xss) = x :: diag (map tail xss)
324324
325325range : Vect n (Fin n)
326−range =
327− reverse range_
328− where
329− range_ : Vect n (Fin n)
330− range_ {n=Z} = Nil
331− range_ {n=(S _)} = last :: map weaken range_
326+range {n=Z} = []
327+range {n=S _} = fZ :: map fS range
332328
333329--------------------------------------------------------------------------------
334330-- Proofs