module test where


open import Data.Nat
open import Data.Product

foo : ℕ → ℕ
foo = λ where
  zero → 1
  (suc x) → 0


bar : ℕ → ℕ
bar  = λ where
  x → {!!}

bar2 : ℕ × ℕ
bar2 .proj₁ = {!!}
bar2 .proj₂ = {!!}