NatToFin, when there is evidence that the conversion will work

Question

The natToFin function from the standard library has the following signature:

 natToFin : Nat -> (n : Nat) -> Maybe (Fin n) 

natToFin 4 5 returns Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5) , while natToFin 5 5 returns Nothing .

I need a function with the following signature:

 myNatToFin : (m : Nat) -> (n : Nat) -> { auto p : n `GT` m } -> Fin n 

It behaves in the same way as the standard lib function, but does not need to return Maybe , because you can always create Fin n from m , given that n greater than m .

How to implement myNatToFin ?

Answer 1

You can do this directly by translating to m , n and the proofs for n `GT` m at the same time:

 import Data.Fin myNatToFin : (m : Nat) -> (n : Nat) -> {auto p : n `GT` m} -> Fin n myNatToFin Z (S n) = FZ myNatToFin (S m) (S n) {p = LTESucc _} = FS $ myNatToFin mn 

Please note that in the second case, you need to match the match to the pattern p (even if its value is not used on the right side) so that you can enter an automatic argument for a recursive call.