Zulip Chat Archive

Stream: new members

Topic: Online theorem prover not printing to console


Derek Gordon (Jun 23 2023 at 20:04):

Hi all, very new to using lean. I am fiddling with https://leanprover.github.io/programming_in_lean/#01_Introduction.html

It evaluates/runs code just fine, but does not print to console. Even when I use the example hello world prgrm it does nothing. Any help greatly appreciated

Derek Gordon (Jun 23 2023 at 20:06):

Hi all, very new to using lean. I am fiddling with https://leanprover.github.io/programming_in_lean/#01_Introduction.html

It evaluates/runs code just fine, but does not print to console. Even when I use the example hello world prgrm it does nothing. Any help greatly appreciated

Notification Bot (Jun 23 2023 at 20:06):

Derek Gordon has marked this topic as resolved.

Notification Bot (Jun 23 2023 at 20:07):

Derek Gordon has marked this topic as unresolved.

Yaël Dillies (Jun 23 2023 at 20:08):

See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Online.20theorem.20prover.20not.20printing.20to.20console

Patrick Massot (Jun 23 2023 at 20:43):

There is no point at all reading this book. It was a great start but was never finished and it covers an obsolete version of Lean. The book Functional programming in Lean 4 is complete and about the current version of Lean.

Notification Bot (Jun 23 2023 at 23:41):

4 messages were moved here from #lean4 > Online theorem prover not printing to console by Scott Morrison.


Last updated: Dec 20 2023 at 11:08 UTC