From 1f04ad1e05ae95a78da458d0268dea08d82e262d Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Sat, 16 Mar 2024 21:58:25 +0200
Subject: idk

---
 Bananas/Basic.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'Bananas/Basic.lean')

diff --git a/Bananas/Basic.lean b/Bananas/Basic.lean
index b972e86..d627107 100644
--- a/Bananas/Basic.lean
+++ b/Bananas/Basic.lean
@@ -92,8 +92,8 @@ section anamorphism
 end anamorphism
 
 section hylomorphism
-  -- partial def hylo (c : φ) (f : β → φ → φ) (g : α → β × α) (p : α → Bool) (a : α) := match p a with
-  --   | true => c
+  -- partial def hylo (c : φ) (f : β → φ → φ) (p : α → Bool) (a : α) := match p a with
+    -- | true => c
     -- | false => let t := g a
               -- f t.fst (hylo c f g p t.snd)
 
@@ -102,12 +102,11 @@ section hylomorphism
   notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f p g
 
   section factorial
-    def p_1 (n : Nat) := decide (n = 0)
-    def g_1 (b : Nat) (hp : ¬p_1 b = true) : Nat × Nat := (b, b-1)
+      def g_1 (b : Nat) (_ : ¬decide (b = 0)) : Nat × Nat := (b, b-1)
 
-    def fac : Nat → Nat := ⟦(1, Nat.mul), (g_1, p_1)⟧
+    def fac : Nat → Nat := ⟦(1, Nat.mul), (g_1, (·=0))⟧
 
-    #eval fac 6
+    #eval fac 8
 
   end factorial
 
-- 
cgit 1.4.1

