------------------------------------------------------------------------
-- Andreas Abel and Brigitte Pientka,
-- Wellfounded Recursion with Copatterns and Sized Types.
--
-- Journal of Functional Programming, volume 26, 2016
--
-- Agda code for examples
------------------------------------------------------------------------

module Prelude where

-- Sizes

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size   #-}
{-# BUILTIN SIZELT   Size<_ #-}
{-# BUILTIN SIZESUC  ↑_     #-}
{-# BUILTIN SIZEINF  ∞      #-}
{-# BUILTIN SIZEMAX  _⊔_   #-}

-- Existential quantification ∃ j < i , A

record ∃< (i : Size) (F : Size → Set) : Set where
  constructor ^
  field {j} : Size< i
        t   : F j

syntax ∃< i (λ j → A) = ∃ j < i , A

-- Unit type

record 𝟙 : Set where

-- Cartesian product type

record _×_ (A B : Set) : Set where
  constructor _,_
  field  fst : A
         snd : B
open _×_ public

-- Natural numbers

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : (n m : ℕ) → ℕ
zero  + m = m
suc n + m = suc (n + m)