diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-06-06 09:23:00 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-06-06 09:23:00 +0200 |
| commit | 51dad2ec627203822e1879e3d58ae5331e58d414 (patch) | |
| tree | c48e1e7abd90f5d9a792f87b07370d9da299a9cd | |
| parent | 91db824bfa4d66f29066a381e88e6e3125e15576 (diff) | |
| download | bidiragda-51dad2ec627203822e1879e3d58ae5331e58d414.tar.gz | |
drop-suc is cong pred
| -rw-r--r-- | Examples.agda | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Examples.agda b/Examples.agda index eca3c90..bda3ae1 100644 --- a/Examples.agda +++ b/Examples.agda @@ -1,6 +1,6 @@ module Examples where -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉ ; pred) open import Data.Nat.Properties using (cancel-+-left) import Algebra.Structures open Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid) @@ -34,11 +34,8 @@ double' = assume-get id↪ (≡-to-Π g) f double'' : Get double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v) -drop-suc : {n m : ℕ} → suc n ≡ suc m → n ≡ m -drop-suc refl = refl - suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ -suc-injection = record { to = ≡-to-Π suc; injective = drop-suc } +suc-injection = record { to = ≡-to-Π suc; injective = cong pred } tail' : Get tail' = assume-get suc-injection (≡-to-Π id) tail |