?

Log in

No account? Create an account
Previous Entry Share Next Entry
Agda2
eye
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₁ : ∀ {l} {a : Set l} → list a → a → a
test₁ ls v = if (not (empty ls)) then head₀ ls else v

test₂ : ∀ {l} {a : Set l} → a → a
test₂ v = head₀ (singleton v) refl
Tags: ,

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

Edited at 2012-05-16 09:46 am (UTC)

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


Чо за фигня?

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

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

  • 1