Zulip Chat Archive
Stream: lean4
Topic: Arithmetic Progression With Lean
Atllkks (Sep 17 2021 at 18:10):
How can I define an arithmetic progression of real numbers ( or generally, a sequence of some real numbers with recursion) a1,a2,..., an for a fixed n in lean?
I am relatively new. Thanks.
Mario Carneiro (Sep 17 2021 at 18:12):
def foo : Nat -> Nat
| 0 => 37
| (n+1) => 2 * foo n
like this?
Last updated: May 02 2025 at 03:31 UTC