Mercurial > hg > Members > atton > agda > systemT
view int.agda @ 4:6b1230883bfa
mini fixes
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 May 2014 14:44:52 +0900 |
parents | 7138e79615b3 |
children | a3cf5cb2b7d3 |
line wrap: on
line source
open import systemT open import Relation.Binary.PropositionalEquality open ≡-Reasoning module int where _+_ : Int -> Int -> Int n + O = n n + (S m) = S (n + m) left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) left-increment n O = refl left-increment n (S m) = cong S (left-increment n m) double : Int -> Int double O = O double (S n) = S (S (double n)) sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n sum-sym O O = refl sum-sym O (S m) = cong S (sum-sym O m) sum-sym (S n) O = cong S (sum-sym n O) sum-sym (S n) (S m) = begin (S n) + (S m) ≡⟨ refl ⟩ S ((S n) + m) ≡⟨ cong S (left-increment n m)⟩ S (S (n + m)) ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩ S (S (m + n)) ≡⟨ sym (cong S (left-increment m n)) ⟩ S ((S m) + n) ≡⟨ refl ⟩ (S m) + (S n) ∎