Zulip Chat Archive
Stream: new members
Topic: Ask for input from user
Michael Wahlberg (Apr 18 2023 at 14:29):
How does one generate functions that ask for input from users in Lean4?
Johan Commelin (Apr 18 2023 at 14:34):
Does https://agentultra.github.io/lean-for-hackers/ help?
Johan Commelin (Apr 18 2023 at 14:34):
Ooh, you might want the Lean 4 version of that site.
Johan Commelin (Apr 18 2023 at 14:34):
https://agentultra.github.io/lean-4-hackers/
Last updated: May 02 2025 at 03:31 UTC