Zulip Chat Archive

Stream: general

Topic: missing commands

Chad McBride (Jul 16 2022 at 19:58):

I have lean4 installed on windows with Visual Studio Code, but some of the commands (from examples) don't seem to be recognized commands. like "universes" isn't recognized but "universe" is.

Kevin Buzzard (Jul 16 2022 at 20:00):

I think universes is no longer a command in bleeding else lean 4

Chad McBride (Jul 16 2022 at 20:02):

Is lean4 a stable version for me to learn on?

Kevin Buzzard (Jul 16 2022 at 20:03):

Lean 4 has not had a release yet, it's in preliminary form. What do you want to learn about?

Kevin Buzzard (Jul 16 2022 at 20:04):

The tutorials for lean 4 come with repos which contain information about exactly which nightly was used to make the project

Chad McBride (Jul 16 2022 at 20:04):

I'm mainly interested to use lean for first-order logic inference.

Kyle Miller (Jul 16 2022 at 20:05):

Which examples are you following?

Chad McBride (Jul 16 2022 at 20:06):

https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html

Last updated: Dec 20 2023 at 11:08 UTC