-- AGDA IN PADOVA

data Bool : Set where
  false : Bool
  true  : Bool
-- This declaration creates a new type, called "Bool".
-- This type has exactly two values: false and true.

data ℕ : Set where  -- \bN
  zero : ℕ
  succ : ℕ → ℕ    -- "succ" is short for "successor"
-- The elements (values, inhabitants) of ℕ are:
-- zero
-- succ zero
-- succ (succ zero)
-- succ (succ (succ zero))
-- ...

-- "pred one" should be zero.
-- "pred (succ (succ zero))" should be one.
-- "pred zero" should be zero.
pred : (a : ℕ) → ℕ
pred zero     = zero
pred (succ n) = n

_+_ : ℕ → ℕ → ℕ
zero   + b = b
succ a + b = succ (a + b)
-- example computation:
-- two + b =
-- succ (succ zero) + b =
-- succ (succ zero + b) =
-- succ (succ (zero + b)) =
-- succ (succ b)

-- "double one" should be succ (succ zero).
-- "double two" should be four.
double : ℕ → ℕ
double zero     = zero
double (succ n) = succ (succ (double n))

double' : ℕ → ℕ
double' x = x + x

-- Agda supports so-called "dependent types": types which depend on values.
-- The prototypical example for a dependent type is the type of vectors of length n.
-- In C, we have the type int[] of arrays of integers. This wouldn't be called a "dependent type",
-- because the dependence is on a type (the type int) and not a value.

-- zero-vector : (n : ℕ) → Vector n
-- zero-vector n = ?

one : ℕ
one = succ zero

-- add2 30 should be 32.
add2 : ℕ → ℕ
add2 n = succ (succ n)

constantly2 : ℕ → ℕ
constantly2 n = succ (succ zero)

data Color : Set where
  red   : Color
  green : Color
  blue  : Color
  pink  : Color

data Empty : Set where
-- The type Empty is empty. There are no values of type Empty.

id : Bool → Bool   -- → \to    α \alpha    ℕ \bN
id x = x
-- in mathematics: sin(5)    id(x)    id(x + y)
-- in Agda:        sin 5     id x     id (x + y)

¬_ : Bool → Bool
¬ false = true
¬ true  = false

-- "and false true" should evaluate to false.
-- "and true  true" should evaluate to true.
_&&_ : Bool → Bool → Bool
false && y     = false
true  && false = false
true  && true  = true

ex : Bool
ex = (¬ false) && true