@@ -38,6 +38,10 @@ weaken : Fin n -> Fin (S n)
3838weaken fZ = fZ
3939weaken (fS k) = fS (weaken k)
4040
41+weakenN : (n : Nat) -> Fin m -> Fin (m + n)
42+weakenN n fZ = fZ
43+weakenN n (fS f) = fS (weakenN n f)
44+
4145strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
4246strengthen {n = S k} fZ = Right fZ
4347strengthen {n = S k} (fS i) with (strengthen i)
@@ -45,6 +49,10 @@ strengthen {n = S k} (fS i) with (strengthen i)
4549 strengthen (fS k) | Right x = Right (fS x)
4650strengthen f = Left f
4751
52+shift : (m : Nat) -> Fin n -> Fin (m + n)
53+shift Z f = f
54+shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)
55+
4856last : Fin (S n)
4957last {n=Z} = fZ
5058last {n=S _} = fS last