From 561de2ba0e83156c172f635f732e6a286ce5126d Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Thu, 15 Jul 2021 14:33:22 +0200
Subject: [PATCH] added nat recursor

---
 personoj/logical.lp |  1 -
 personoj/nat.lp     | 10 ++++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/personoj/logical.lp b/personoj/logical.lp
index c3db436..c7ebe31 100644
--- a/personoj/logical.lp
+++ b/personoj/logical.lp
@@ -14,4 +14,3 @@ rule if {prop} $p $then $else ↪ ($p ⇒ $then) ⇒ (λ _, (¬ $p) ⇒ $else);
 symbol iff P Q ≔ (P ⇒ (λ _, Q)) ∧ (λ _, Q ⇒ (λ _, P));
 
 symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λ x, ¬ (P x)));
-
diff --git a/personoj/nat.lp b/personoj/nat.lp
index 28a4449..dcf50b6 100644
--- a/personoj/nat.lp
+++ b/personoj/nat.lp
@@ -9,3 +9,13 @@ rule eqnat (succ $n) (succ $m) ↪ eqnat $n $m
 with eqnat zero (succ _) ↪ false
 with eqnat (succ _) zero ↪ false
 with eqnat zero zero ↪ true;
+
+// Recursor on integers
+symbol nrec {t: Set} : Nat → El t → (Nat → El t → El t) → El t;
+rule nrec {$t} (succ $n) $base $f ↪ $f $n (nrec {$t} $n $base $f);
+rule nrec zero $base _ ↪ $base;
+
+// We introduce an object level Nat to have polymorphism on the recursor.
+symbol nat/o: Set;
+rule El nat/o ↪ Nat;
+symbol + (sn m: Nat) ≔ nrec sn m (λ _ npm, succ npm); notation + infix 6;
-- 
GitLab