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

diff 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
line wrap: on
line diff
--- a/nat.agda	Wed Aug 07 09:50:51 2019 +0900
+++ b/nat.agda	Wed Aug 07 10:28:33 2019 +0900
@@ -38,3 +38,9 @@
 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
 
+max : (x y : Nat) → Nat
+max Zero Zero = Zero
+max Zero (Suc x) = (Suc x)
+max (Suc x) Zero = (Suc x)
+max (Suc x) (Suc y) = Suc ( max x y )
+