848d66d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Replace Prelude.Vect.take and Prelude.Vect.drop with versions of a saner type signature.

848d66dStephen Drodge13 years ago

libs/prelude/Prelude/Vect.idr+14−9

compare with master

unifiedsplit

@@ -51,15 +51,14 @@ replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

51-- Subvectors

52--------------------------------------------------------------------------------

54−take : Fin n -> Vect n a -> (p ** Vect p a)

54+take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a

55−take fZ xs = (_ ** [])

55+take (fS k) [] = FinZElim k

56−take (fS k) [] impossible

56+take fZ _ = []

57−take (fS k) (x::xs) with (take k xs)

57+take (fS k) (x::xs) = x :: take k xs

58− | (_ ** tail) = (_ ** x::tail)

58+

59−

60−drop : Fin n -> Vect n a -> (p ** Vect p a)

59+drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a

61−drop fZ xs = (_ ** xs)

62−drop (fS k) [] impossible

60+drop (fS k) [] = FinZElim k

61+drop fZ xs ?= xs

63drop (fS k) (x::xs) = drop k xs

62drop (fS k) (x::xs) = drop k xs

65--------------------------------------------------------------------------------

64--------------------------------------------------------------------------------

@@ -311,6 +310,12 @@ range {n=S _} = fZ :: map fS range

311-- Proofs

310-- Proofs

312--------------------------------------------------------------------------------

311--------------------------------------------------------------------------------

313

312

313+Prelude.Vect.drop_lemma_1 = proof {

314+ intros;

315+ rewrite sym (minusZeroRight n);

316+ trivial;

317+}

318+

314Prelude.Vect.reverse'_lemma_2 = proof {

319Prelude.Vect.reverse'_lemma_2 = proof {

315 intros;

320 intros;

316 rewrite (plusSuccRightSucc m n1);

321 rewrite (plusSuccRightSucc m n1);