@@ -38,6 +38,10 @@ weaken : Fin n -> Fin (S n)
38weaken fZ = fZ
38weaken fZ = fZ
39weaken (fS k) = fS (weaken k)
39weaken (fS k) = fS (weaken k)
41+weakenN : (n : Nat) -> Fin m -> Fin (m + n)
43+weakenN n (fS f) = fS (weakenN n f)
41strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
45strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
42strengthen {n = S k} fZ = Right fZ
46strengthen {n = S k} fZ = Right fZ
43strengthen {n = S k} (fS i) with (strengthen i)
47strengthen {n = S k} (fS i) with (strengthen i)
@@ -45,6 +49,10 @@ strengthen {n = S k} (fS i) with (strengthen i)
45 strengthen (fS k) | Right x = Right (fS x)
49 strengthen (fS k) | Right x = Right (fS x)
46strengthen f = Left f
50strengthen f = Left f
52+shift : (m : Nat) -> Fin n -> Fin (m + n)
54+shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)
48last : Fin (S n)
56last : Fin (S n)
49last {n=Z} = fZ
57last {n=Z} = fZ
50last {n=S _} = fS last
58last {n=S _} = fS last