the nattofin function standard library has 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 function following signature:
mynattofin : (m : nat) -> (n : nat) -> { auto p : n `gt` m } -> fin n it behaves same standard lib function doesn't need return maybe because possible generate fin n m given n greater m.
how implement mynattofin?
you can directly recursing on m, n, , evidence n `gt` m @ 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 m n note need pattern match on p in second case (even though value not used on right-hand side) automatic argument recursive call can filled in.
