Как работи това в agda?

Нека направим дисекция на thm2.

Видът на израза

∃ λ m → m < 10

∃ е дефиниран в Data.Product като псевдоним за Σ, където първият аргумент остава неявен. Това означава, че ∃ взема елемент B от тип A → Set и връща типа двойки, съдържащи a от тип A и b от тип B a.

Сега λ m → m < 10 взема m в ℕ и връща типа доказателства, които m < 10.

Така че ∃ λ m → m < 10 е типът двойки на ℕ и доказателство, че е по-малко от 10.

Самият израз

zero , s≤s z≤n

За цялата проверка на типа ни трябва:

zero да бъде ℕ, което е.

s≤s z≤n да бъде доказателство, че 0 < 10. _<_ е дефиниран в Data.Nat.Base като псевдоним за λ m n → suc m ≤ n. Така че доказването на 0 < 10 е същото като доказването на това 1 ≤ 10.

Сега _≤_ е индуктивен тип с два конструктора:

• основен случай z≤n, който казва, че 0 е по-малко от или равно на всички естествени числа
• случай на стъпка s≤s, който казва, че ако едно число е по-малко отколкото или равно на друго, тогава техните sucs също са по-малки или равни.

Доказателството s≤s z≤n наистина е валидно доказателство, че 1 ≤ 10: z≤n доказва, че 0 ≤ 9 и s≤s заключава, че следователно 1 ≤ 10.