Понимание `k: Nat ** 5 * k = n` Подпись

Question

Следующая функция компилирует:

onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat
onlyModByFive n k = 100

Но что делает k представлять с его Nat ** 5 * k = n синтаксис?

Кроме того, как я могу назвать это? Вот что я пробовал, но я не понимаю вывод.

*Test> onlyModByFive 5 5
When checking an application of function Main.onlyModByFive:
        (k : Nat ** plus k (plus k (plus k (plus k (plus k 0)))) = 5) is not a
        numeric type

источник ответа - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ

Answer 1

(k : Nat) ** (5 * k = n) является зависимой парой, состоящей из

• Первый элемент k : Nat
• Второй элемент prf : 5 * k = n

Другими словами, это экзистенциальный тип, который говорит "существует k : Nat такой, что 5 * k = n". Чтобы быть конструктивным, вы должны дать такой k и доказательство того, что оно действительно удовлетворяет 5 * k = n,

В вашем примере, если вы частично подаете заявку onlyModByFive в 5, вы получаете что-то типа

onlyModModByFive 5 : ((k : Nat) ** (5 * k = 5)) -> Nat

поэтому второй аргумент должен быть типа (k : Nat) ** (5 * k = 5), Есть только один выбор k мы можем сделать здесь, установив его 1и доказывая, что 5 * 1 = 5:

foo : Nat
foo = onlyModByFive 5 (1 ** Refl)

Это работает, потому что 5 * 1 сводится к 5так что мы должны доказать 5 = 5что можно сделать тривиально, используя Refl : a = a напрямую (объединяющий a ~ 5).