module Bool where

-- file must start with module declaration coinciding with filename, agda-mode

data Bool : Set where
  true  : Bool
  false : Bool 

-- type-check, menu eller ^C ^L ! note colors (brown, green, blue)
-- cf Haskell's data, need more flexible syntax because of dependent types
-- note Bool : Set, declares the type of Bool!

not : Bool → Bool
not true  = false
not false = true

-- function arrow -> can be written with unicode symbol ‚Üí 
-- by writing latex code \to.

-- We cannot write partial functions in Agda: 

-- loop : Bool -> Bool
-- loop x = loop x

-- fixBool : (Bool → Bool) → Bool
-- fixBool f = f (fixBool f)

-- orange means failed termination check, means "warning: may not terminate!"

-- using ?. If you don't know the definition you can do gradual refinements

f : Bool → Bool
f x = not (not x)

-- two ways of filling in the hole: 
-- 1. "give" put a term x in the hole and do ^C ^SPC which checks the type
-- 2. "refine" put a term not in the hole and do ^C ^R

-- automatic case split, do ^C ^C and the system will ask for the variable 

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

-- show goal type ^C C,

-- h : Bool → Bool
-- h x = {!!}

-- normalise: not true ^C ^N
-- goto definition: M . place cursor on "not"

-- case analysis in two arguments, infix notation

_<==>_ : Bool → Bool → Bool
true  <==> true  = true
true  <==> false = false
false <==> true  = false
false <==> false = true

-- mixfix

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