-- Functions.Cases exercises -- By Xiaoning Bian module Functions.Cases where -- I write my own -- open import Sets.Enumerated using (Bool; true; false) data Bool : Set where true : Bool false : Bool not : Bool → Bool not true = false not false = true _∧_ : Bool → Bool → Bool true ∧ x = x false ∧ _ = false infixr 6 _∧_ -- Exercise: _∨_ -- Define logical OR: _∨_ : Bool → Bool → Bool true ∨ true = true true ∨ false = true false ∨ true = true false ∨ false = true infixr 5 _∨_ -- Define logical OR with one alternative, with the help of not and _∧_! _∨'_ : Bool → Bool → Bool a ∨' b = not (a ∧ b) -- Define a set named Answer with three elements, yes, no and maybe. data Answer : Set where yes : Answer no : Answer maybe : Answer -- Define logical operations on Answer! not' : Answer → Answer not' yes = no not' no = yes not' maybe = maybe -- Define a set named Quarter with four elements, east, west, north and south. data Quarter : Set where east : Quarter west : Quarter north : Quarter south : Quarter -- Define a function turnLeft : Quarter → Quarter. turnLeft : Quarter → Quarter turnLeft east = north turnLeft west = south turnLeft north = west turnLeft south = east -- Define the functions turnBack and turnRight with the help of turnLeft! (By either pattern matching or defining a specific function composition function.) turnBack : Quarter → Quarter turnBack east = west turnBack west = east turnBack north = south turnBack south = north turnRight : Quarter → Quarter turnRight a = turnLeft (turnBack a)