Mercurial > hg > Members > kono > Proof > galois

comparison nat.agda @ 210:2eb62a2a34f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 05 Dec 2020 09:41:16 +0900
parents 43731a549950
children
comparison
equal deleted inserted replaced
209:40695d752dd0 210:2eb62a2a34f2
50 <-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n) 50 <-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
51 <-∨ {suc x} {zero} (s≤s ()) 51 <-∨ {suc x} {zero} (s≤s ())
52 <-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt 52 <-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
53 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) 53 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
54 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) 54 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
55
56 n≤n : (n : ℕ) → n Data.Nat.≤ n
57 n≤n zero = z≤n
58 n≤n (suc n) = s≤s (n≤n n)
59
60 <→m≤n : {m n : ℕ} → m < n → m Data.Nat.≤ n
61 <→m≤n {zero} lt = z≤n
62 <→m≤n {suc m} {zero} ()
63 <→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)
55 64
56 max : (x y : ℕ) → ℕ 65 max : (x y : ℕ) → ℕ
57 max zero zero = zero 66 max zero zero = zero
58 max zero (suc x) = (suc x) 67 max zero (suc x) = (suc x)
59 max (suc x) zero = (suc x) 68 max (suc x) zero = (suc x)