From 1f04ad1e05ae95a78da458d0268dea08d82e262d Mon Sep 17 00:00:00 2001 From: tzlil Date: Sat, 16 Mar 2024 21:58:25 +0200 Subject: idk --- Bananas/Basic.lean | 11 +++++------ 1 file 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 -- cgit 1.4.1