@@ -65,6 +65,11 @@ weakenN : (n : Nat) -> Fin m -> Fin (m + n)
6565weakenN n FZ = FZ
6666weakenN n (FS f) = FS (weakenN n f)
6767
68+||| Weaken the bound on a Fin using an inequality proof
69+weakenLTE : LTE n m -> Fin n -> Fin m
70+weakenLTE (LTESucc p) FZ = FZ
71+weakenLTE (LTESucc p) (FS f) = FS $ weakenLTE p f
72+
6873||| Attempt to tighten the bound on a Fin.
6974||| Return `Left` if the bound could not be tightened, or `Right` if it could.
7075strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
@@ -101,6 +106,10 @@ implementation MinBound (Fin (S n)) where
101106implementation MaxBound (Fin (S n)) where
102107 maxBound = last
103108
109+||| Add two Fins
110+addFin : (x : Fin n) -> (y : Fin m) -> Fin (finToNat x + m)
111+addFin FZ y = y
112+addFin (FS x) y = FS $ addFin x y
104113
105114-- Construct a Fin from an integer literal which must fit in the given Fin
106115