2021-01-27 14:44:46 -08:00

#### 40 lines 930 B Idris Raw Permalink Blame History

 ```module HomeworkFour ``` ```%default total ``` ```%access public export ``` ``` ``` ```even : Nat -> Bool ``` ```even Z = True ``` ```even (S Z) = False ``` ```even (S (S n)) = even n ``` ``` ``` ```evenSuc : even n = True -> even (S n) = False ``` ```evenSuc {n=Z} Refl = Refl ``` ```evenSuc {n=S Z} Refl impossible ``` ```evenSuc {n=S (S m)} p = evenSuc {n=m} p ``` ``` ``` ```oddSuc : even n = False -> even (S n) = True ``` ```oddSuc {n=Z} Refl impossible ``` ```oddSuc {n=S Z} Refl = Refl ``` ```oddSuc {n=S (S m)} p = oddSuc {n=m} p ``` ``` ``` ```evenFlip : even n = b -> even (S n) = not b ``` ```evenFlip {n=Z} Refl = Refl ``` ```evenFlip {n=S Z} Refl = Refl ``` ```evenFlip {n=S (S m)} p = evenFlip {n=m} p ``` ``` ``` ```evenFlip' : even n = b -> even (S n) = not b ``` ```evenFlip' {b=True} p = evenSuc p ``` ```evenFlip' {b=False} p = oddSuc p ``` ``` ``` ```evenSucSuc : even n = True -> even (S (S n)) = True ``` ```evenSucSuc p = p ``` ``` ``` ```oddSucSuc : even n = False -> even (S (S n)) = False ``` ```oddSucSuc p = p ``` ``` ``` ```evenStay : even n = b -> even (S (S n)) = b ``` ```evenStay p = p ``` ``` ``` ```evenStayEq : even n = even (S (S n)) ``` ```evenStayEq = Refl ```