Zulip Chat Archive

Stream: general

Topic: Helloworld from PIL book


view this post on Zulip Daniel Donnelly (Aug 30 2019 at 23:56):

https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf
page 7
Code is:

import system.io
variable [io.interface]
open io
def hello_world : io unit :=
put_str "hello world\n"
#eval hello_world

But it doesn't even like the second line. So how can I learn from this book? I am assuming if I overcome a few examples, I'll be able to fix the rest on my own.

view this post on Zulip Jeremy Avigad (Aug 31 2019 at 00:32):

PIL is badly outdated, and I haven't been able to find the time to update it. The information in this paper may be more up to date: https://leanprover.github.io/papers/tactic.pdf.

view this post on Zulip Jeremy Avigad (Aug 31 2019 at 00:36):

Patrick Massot has written a nice tutorial: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md.
It might also help to look at examples in mathlib: https://github.com/leanprover-community/mathlib/tree/master/src/tactic.
In the particular case you mention, deleting the second line fixes the problem.


Last updated: May 08 2021 at 10:12 UTC