Mercurial > hg > Members > kono > Proof > HyperReal
changeset 11:2ce1c67dde0f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Jul 2021 15:53:55 +0900 |
| parents | a4e441b7493b |
| children | e607f453f607 |
| files | src/HyperReal.agda |
| diffstat | 1 files changed, 3 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/HyperReal.agda Sun Jul 04 15:47:18 2021 +0900 +++ b/src/HyperReal.agda Sun Jul 04 15:53:55 2021 +0900 @@ -34,8 +34,9 @@ record NN ( i j k : ℕ) : Set where field - nn : (k + j ) * (k + suc j ) + j * 2 ≡ i * 2 - ni : i ≡ 0 → j ≡ 0 + stage : ℕ + nn : j + k ≡ stage + ni : i ≡ stage + k i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 i≤0→i≡0 {0} z≤n = refl