natToFin, когда есть доказательства того, что преобразование будет работать

Question

natToFin В функции из стандартной библиотеки имеет следующую подпись:

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

natToFin 4 5 возвращается Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5), в то время как natToFin 5 5 возвращается Nothing.

Я хотел бы функцию со следующей подписью:

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

Он ведет себя так же, как стандартные Lib функции, но не нужно возвращать Maybe, потому что всегда можно генерировать Fin n из m что n больше, чем m.

Как осуществить myNatToFin?

Answer 1

Вы можете сделать это непосредственно рекурсии на m, n, и доказательства n `GT` m в то же время:

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 

Обратите внимание, что вам нужно шаблон матч на p во втором случае (даже если его значение не используется в правой части), так что автоматический аргумент для рекурсивного вызова может быть заполнен.