{-# OPTIONS --guardedness #-}

-- inspired by https://blog.ielliott.io/lambdas-are-codatatypes
-- with thanks to Philip for showing me the above (I was coerced to write this line)

open import Data.Nat using (ℕ ; suc)

record Lambda (A B : Set) : Set where
  coinductive
  field
    apply : A → B

open Lambda

+1 : Lambda ℕ ℕ
apply +1 n = suc n