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: Dec 20 2023 at 11:08 UTC