Mercurial > hg > Members > kono > Proof > prob1
changeset 19:9f5bf86fe6dd
fix uniquness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 28 Mar 2020 13:38:56 +0900 |
| parents | e35d729efd58 |
| children | 9cd63570c1ba |
| files | nat.agda prob1.agda |
| diffstat | 2 files changed, 8 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Mar 27 14:37:08 2020 +0900 +++ b/nat.agda Sat Mar 28 13:38:56 2020 +0900 @@ -8,7 +8,7 @@ open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import logic -open import Relation.Binary.Definitions +-- open import Relation.Binary.Definitions nat-<> : { x y : ℕ } → x < y → y < x → ⊥ nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
--- a/prob1.agda Fri Mar 27 14:37:08 2020 +0900 +++ b/prob1.agda Sat Mar 28 13:38:56 2020 +0900 @@ -9,8 +9,15 @@ open import Data.Empty open import Data.Product open import Relation.Nullary +<<<<<<< working copy + +||||||| base + + +======= open import Relation.Binary.Definitions +>>>>>>> destination -- All variables are positive integer -- A = -M*n + i +k*M - M -- where n is in range (0,…,k-1) and i is in range(0,…,M-1)