{-# OPTIONS --allow-unsolved-meta #-}
open import Agda.Primitive
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
double : ℕ → ℕ
double zero = zero
double (succ n) = succ (succ (double n))
id : {A : Set} → (A → A)
id x = x
ex : ℕ
ex = id {ℕ} zero
data Vector (A : Set) : ℕ → Set where
[] : Vector A zero
_∷_ : {n : ℕ} → A → Vector A n → Vector A (succ n)
two : ℕ
two = succ (succ zero)
ex₂ : Vector ℕ two
ex₂ = two ∷ (zero ∷ [])
_+_ : ℕ → ℕ → ℕ
zero + b = b
succ a + b = succ (a + b)
data Bool : Set where
false true : Bool
is-even? : ℕ → Bool
is-even? zero = true
is-even? (succ zero) = false
is-even? (succ (succ n)) = is-even? n
is-eq? : ℕ → ℕ → Bool
is-eq? zero zero = true
is-eq? zero (succ b) = false
is-eq? (succ a) zero = false
is-eq? (succ a) (succ b) = is-eq? a b
is-eq?? : (ℕ → ℕ) → (ℕ → ℕ) → Bool
is-eq?? f g = {!!}
replicate : {X : Set} → (n : ℕ) → X → Vector X n
replicate zero x = []
replicate (succ n) x = x ∷ replicate n x
data Even : ℕ → Set where
base : Even zero
step : {n : ℕ} → Even n → Even (succ (succ n))
postulate
whatever : Even (succ zero)
four-is-even : Even (succ (succ (succ (succ zero))))
four-is-even = step (step base)
even-numbers-are-even : {n : ℕ} → Even n → Even n
even-numbers-are-even p = p
double-x-is-even : (n : ℕ) → Even (double n)
double-x-is-even zero = base
double-x-is-even (succ n) = step (double-x-is-even n)
thm : Even (succ (succ zero))
thm = double-x-is-even (succ zero)
data _≡_ {ℓ : Level} {X : Set ℓ} : X → X → Set where
refl : {x : X} → x ≡ x
lemma₀ : (zero + zero) ≡ zero
lemma₀ = refl
lemma₁ : (b : ℕ) → (zero + b) ≡ b
lemma₁ b = refl
cong
: {ℓ : Level} {X Y : Set ℓ} {a b : X}
→ (f : X → Y) → a ≡ b → f a ≡ f b
cong f refl = refl
lemma₂ : (a : ℕ) → (a + zero) ≡ a
lemma₂ zero = refl
lemma₂ (succ a) = cong succ (lemma₂ a)
foo : ℕ → (b : ℕ) → ℕ → is-even? b ≡ true → Vector ℕ b
foo a b c p = {!!}
foo' : ℕ → (b : ℕ) → ℕ → Even b → Vector ℕ b
foo' a b c p = {!!}
data List (X : Set) : Set where
[] : List X
_∷_ : X → List X → List X
length : {X : Set} → List X → ℕ
length [] = zero
length (x ∷ xs) = succ (length xs)
fib : ℕ → ℕ
fib zero = zero
fib (succ zero) = succ zero
fib (succ (succ n)) = fib n + fib (succ n)
data IsFibonacci : ℕ → Set where
bar : (a : ℕ) → IsFibonacci (fib a)
foo'' : {X : Set} → (xs : List X) → IsFibonacci (length xs) → {!!}
foo'' = {!!}
open import Data.Product
foo''' : {X : Set} → (xs : List X) → Σ[ a ∈ ℕ ] (length xs ≡ fib a) → {!!}
foo''' = {!!}