Simplify Prelude.Vect.range
commit8bc1c7fa717af1b155603432a06d1e8d52931b8a
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateSun 28 Jul 2013, 19:36 (13 years ago)
parent02367f9
lib/Prelude/Vect.idr+2−6
@@ -322,12 +322,8 @@ diag [] = []
322322diag ((x::xs)::xss) = x :: diag (map tail xss)
323323
324324range : Vect n (Fin n)
325−range =
326− reverse range_
327− where
328− range_ : Vect n (Fin n)
329− range_ {n=Z} = Nil
330− range_ {n=(S _)} = last :: map weaken range_
325+range {n=Z} = []
326+range {n=S _} = fZ :: map fS range
331327
332328--------------------------------------------------------------------------------
333329-- Proofs