----------------------------------
-- Power example for NBE-lectures
----------------------------------

module Palmse.Power where

open import Data.Nat
open import Palmse.Product
-- open import Data.Product
-- open import Data.Unit

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

power : ℕ -> ℕ -> ℕ
power m 0       = 1
power m (suc n) = m * (power m n)

infixr 4 _^_

_^_ :  ℕ -> ℕ -> ℕ
m ^ 0       = 1
m ^ (suc n) = (m ^ n) * m

-- Do C-c C-n- \m -> power m 3 and you get the normal form (secondary 
-- school simplification)

-- Now an example of a dependent type, which also shows how
-- types can be computed and normalized:

Power : Set -> ℕ -> Set
Power A 0       = N₁
Power A (suc n) = A × (Power A n)

-- Do C-c C-n- \A -> Power A 3

Date : Set
Date = Power ℕ 3

-- Do C-c C-n- Power ℕ 3

today : Date
today = 2009 , 3 , 30 , 0₁