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
|
