Agda2

[voidex]

Ковыряю Agda2
module if where open import proof open import bool open import list if_then_else_ : ∀ {l} {a : Set l} → (p : bool) → ((p ≡ true) → a) → a → a if true then t else f = t refl if false then t else f = f head₀ : ∀ {l} {a : Set l} → (ls : list a) → (not (empty ls) ≡ true) → a head₀ {_} {_} null () head₀ {_} {_} (cons x xs) p = x test₁

Comments

[udpn]

И чо, компилится? У тебя ж head₀ принимает два явных параметра, а внутри test₁ ты второй не передаёшь.

[voidex]

Так в true-ветке if передаётся этот пруф (t refl).

[udpn]

Чо за фигня?

[voidex]

Не понял вопрос.
if вторым параметром принимает функцию от одного аргумента. head0 ls и есть таковая, она принимает на вход пруф, что список не пуст, возвращает голову.
В test2 мы этот пруф передаём сами (refl), в test1 это делает if. Мы не можем в test1 написать так же, как в test2, потому что список у нас там, в общем случае, любой. Но вот if сам уже имеет такое доказательство, так как, собственно, матчится по тому, выполняется условие или нет, и потому может его передать (t refl).
refl - тривиальное док-во, x == x.

[krasnogorr]

Какой ты единомышленник??77 ты сектант!!!111