open import Data.Nat renaming (ℕ to Nat)
open import Data.Bool

data  List (a : Set) : Set where
  Nil : List a                  -- () → A ≅ A
  Cons :  a → List a → List a

data Tree (a : Set) : Set where
  Leaf : a → Tree a
  Inner : a → Tree a → Tree a → Tree a

-- 1.2a
length : {!!}
length Nil = 0
length (Cons x xs) = 1 + length xs

size : {!!}
size (Leaf x) = 1
size (Inner x l r) = 1 + size l + size r

-- 1.2b
-- length (Cons 4 (Cons 89 (Cons 21 Nil)))

-- 1.3
element : Nat → List Nat → Bool
element = {!!}

-- 2
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

foldL : ∀ {a c : Set} →
          c → (a → c → c) → List a → c
foldL n f Nil = n
foldL n f (Cons x xs) = f x (foldL n f xs)

-- 2.1
norm : ∀ (n : {!!}) (f : {!!}) →
  foldL n f (Cons 2 (Cons 3 (Cons 6 Nil))) ≡ {!!}
norm n f = begin
  foldL n f (Cons 2 (Cons 3 (Cons 6 Nil))) ≡⟨⟩
  {!!} ≡⟨⟩
  {!!} ∎

-- 2.2
foldT : {!!}
foldT = {!!}

-- 2.3
length' : {!!}
length' = foldL {!!} {!!}

size' : {!!}
size' = {!foldT!}