module IType.Bool where open import IType.Nat data Bool : Set where true : Bool false : Bool -- Note that Agda has a standard library where many common types and functions are defined 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 ¬ = not -- 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 _||_ : Bool → Bool → Bool true || true = true false || true = true true || false = true false || false = false -- It is a special case of mixfix declarations: if_then_else_ : {C : Set} → Bool → C → C → C 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! eqNat : Nat → Nat → Bool eqNat zero zero = true eqNat zero (succ n) = false eqNat (succ m) zero = false eqNat (succ m) (succ n) = eqNat m n isZero : Nat → Bool isZero n = natrec true (λ x y → false) n help : (Nat → Bool) → Nat → Bool help f zero = false help f (succ n) = f n eqNat' : Nat → Nat → Bool eqNat' zero = isZero eqNat' (succ m) = help (eqNat' m) open import MLTT.PropositionalLogic So : Bool → Set So true = ⊤ So false = ⊥ ||-intro : (b c : Bool) → So b → So (b || c) ||-intro true true ⊤-intro = ⊤-intro ||-intro true false ⊤-intro = ⊤-intro ||-intro false c () refleqNat : (n : Nat) → So (eqNat n n) refleqNat zero = ⊤-intro refleqNat (succ n) = refleqNat n _<_ : Nat → Nat → Bool m < zero = false zero < succ n = true succ m < succ n = m < n