-- Each file is a module with the same name as the file
-- We thus declare

module Bool where

-- We can define data types in a similar way as in Haskell,
-- but the syntax is different since we have more general types in Agda.
-- In Haskell we can declare
-- data Bool = True | False
-- but in Agda we have a more verbose syntax:

data Bool : Set where
  true  : Bool
  false : Bool

-- Note that Agda has a standard library where many common types and functions are defined

-- We can also define functions in Agda much like in Haskell, 
-- but whereas Haskell infers the type of a function, we must declare it in Agda:

not : Bool -> Bool
not true = false
not false = true

-- In Agda we have unicode and can for example write 
-- → for -> and ¬ for not: 

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

-- The names of unicode characters used by Agda are often the same as the names used in latex.

-- In Agda, we can write programs by gradual refinement, 
-- where we write ? for an unknown part of the program.
-- The ? becomes { - } when type-checked (a "hole").
-- Holes can be filled in either by writing a complete expression in the hole and doing ^C^SPC
-- or by writing a partial expression in the whole and doing ^C^R (refine)
-- or by writing the top level function and doing ^C^R

-- Exercise: write the following function by gradual refinement:

¬¬ : Bool → Bool
¬¬ b = ¬ (¬ b)

-- Agda can also create complete case analysis (pattern matching) automatically 
-- by writing the pattern variable in a hole and do ^C^C

-- Exercise: write not by gradual refinement and case analysis

-- This is how you declare an infix operator:

_&&_ : Bool → Bool → Bool
b && true  = b
b && false = false

-- It is a special case of mixfix declarations:

if_then_else_ : Bool → Bool → Bool → Bool
if true  then y else z = y
if false then y else z = z

-- You can compute ("normalize") closed expressions by writing ^C^N and then write the expression afterwards.

-- Exercise: compute a few expressions!