Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison nat.agda @ 220:95a26d1698f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try to separate Ordinals
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Aug 2019 10:28:33 +0900
parents 22d435172d1a
children
comparison
equal deleted inserted replaced
219:43021d2b8756 220:95a26d1698f4
36 <-∨ {Suc x} {Zero} (s≤s ()) 36 <-∨ {Suc x} {Zero} (s≤s ())
37 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt 37 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
38 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) 38 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
39 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) 39 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
40 40
41 max : (x y : Nat) → Nat
42 max Zero Zero = Zero
43 max Zero (Suc x) = (Suc x)
44 max (Suc x) Zero = (Suc x)
45 max (Suc x) (Suc y) = Suc ( max x y )
46