michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix to RelationsAns

Browse source
This commit is contained in:
wadler 2018-03-06 18:38:27 -03:00
parent bcc8e78eb4
commit ea44518e27
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/RelationsAns.lagda
View file

@ -9,7 +9,7 @@ permalink : /RelationsAns
\begin{code}
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
open import Relations using (_≤_; _<_; Trichotomy; even; odd)
open import Properties using (+-comm; +-identity; +-suc)
open import Data.Nat.Properties using (+-comm; +-identityʳ; +-suc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Data.Product using (∃; _,_)
open Trichotomy
@ -64,7 +64,7 @@ trichotomy (suc m) (suc n) with trichotomy m n
\begin{code}
+-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
+-lemma m rewrite +-identity m | +-suc m m = refl
+-lemma m rewrite +-identityʳ m | +-suc m m = refl
+-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
+-lemma′ m rewrite +-suc m (m + 0) = {!!}