{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude

module Nat where

infixl 10 _+_ _-_
infixl 11 _*_
infixr 12 _^_


data  : Set where
  O : 
  S :   

{-# BUILTIN NATURAL  #-}
{-# BUILTIN ZERO    O #-}
{-# BUILTIN SUC     S #-}

natcases : {A :   Set}  A O  ((n : )  A (S n))  Π  A
natcases a f O     = a
natcases a f (S n) = f n

-----------------------------------------------

_+_         : Op 
O + n       = n
S m + n     = S (m + n)

{-# BUILTIN NATPLUS _+_ #-}

_-_ : Op 
m   - O   = m
O   - n   = O
S m - S n = m - n

{-# BUILTIN NATMINUS _-_ #-}

_*_ : Op 
O   * n = O
S m * n = n + m * n

{-# BUILTIN NATTIMES _*_ #-}

_^_ : Op 
m ^ O = 1
m ^ (S n) = m * m ^ n


data ℕ⁺ : Set where
  S :   ℕ⁺

_-1 : ℕ⁺  
(S n) -1 = n

ℕ⁺toℕ : ℕ⁺  
ℕ⁺toℕ (S n) = S n



open import List

replicate : {A : Set}    A  List A
replicate O     a = []
replicate (S n) a = a  replicate n a

length : {A : Set}  List A  
length = foldr (const S) O

sum : List   
sum = foldr _+_ 0

product : List   
product = foldr _*_ 1

replicateL : {A : Set}    List A  List A
replicateL n = concat  replicate n

open import Bool

count : {A : Set}  (A  Bool)  List A  
count p = foldr (\ a  if p a then S else id) O