From a9b4fa26887b070f5423caee38c8b3eeceb78352 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 6 Jul 2016 13:06:00 +0200 Subject: [PATCH] add equalNat --- examples/nat.ctt | 9 +++++++++ 1 file changed, 9 insertions(+) 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 -- 2.34.1