VoidEx (voidex) wrote,
VoidEx
voidex

Agda2

Ковыряю 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: agda, fp
Subscribe
  • Post a new comment

    Error

    default userpic
    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 5 comments