diff options
| -rw-r--r-- | Bananas/Basic.lean | 11 |
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 |