From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 6 Jul 2016 11:06:00 +0000 (+0200)
Subject: add equalNat
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a9b4fa26887b070f5423caee38c8b3eeceb78352;p=cubicaltt.git

add equalNat
---

diff --git a/examples/nat.ctt b/examples/nat.ctt
index db26e94..d38334a 100644
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -1,6 +1,7 @@
 module nat where
 
 import hedberg
+import bool
 
 data nat = zero | suc (n : nat)
 
@@ -83,3 +84,11 @@ natDec : (n m:nat) -> dec (Id nat n m) = split
                  (sucInj n m) (natDec n m))
 
 natSet : set nat = hedberg nat natDec
+
+equalNat : nat -> nat -> bool = split
+    zero -> split@(nat -> bool) with
+      zero  -> true
+      suc n -> false
+    suc m -> split@(nat -> bool) with
+      zero  -> false
+      suc n -> equalNat m n