@@ -323,12 +323,8 @@ diag [] = []
323diag ((x::xs)::xss) = x :: diag (map tail xss)
323diag ((x::xs)::xss) = x :: diag (map tail xss)
325range : Vect n (Fin n)
325range : Vect n (Fin n)
326−range =
326+range {n=Z} = []
327− reverse range_
327+range {n=S _} = fZ :: map fS range
329− range_ : Vect n (Fin n)
331− range_ {n=(S _)} = last :: map weaken range_
333--------------------------------------------------------------------------------
329--------------------------------------------------------------------------------