summary refs log tree commit diff
diff options
context:
space:
mode:
-rw-r--r--Bananas/Basic.lean11
1 files changed, 5 insertions, 6 deletions
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