@@ -322,12 +322,8 @@ diag [] = []
322diag ((x::xs)::xss) = x :: diag (map tail xss)
322diag ((x::xs)::xss) = x :: diag (map tail xss)
324range : Vect n (Fin n)
324range : Vect n (Fin n)
325−range =
325+range {n=Z} = []
326− reverse range_
326+range {n=S _} = fZ :: map fS range
328− range_ : Vect n (Fin n)
330− range_ {n=(S _)} = last :: map weaken range_
332--------------------------------------------------------------------------------
328--------------------------------------------------------------------------------