search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

Some outdated code in the tutorial. #4

Closed benjamin20104 closed 3 years ago

benjamin20104 commented 3 years ago

Chapter 3 Propositions and Proofs uses Or.intro_left, Or.intro_right, and Or.elim pretty heavily, but I believe they are no longer supported in Lean4.

Kha commented 3 years ago

It is your Lean 4 version that is outdated, not the tutorial :) https://github.com/leanprover/lean4/blob/075ba63a8b4653a5152917cef028b0695f2b471d/src/Init/Prelude.lean#L145-L154. Try updating to the latest nightly.

benjamin20104 commented 3 years ago

Ah thanks, I apologize for not doing my research. Still, while trying to install the nightly build I've run into the following error: dyld: Library not loaded: /Users/runner/work/lean4/lean4/build/stage1/lib/lean/libleanshared.dylib. Not sure if this has anything to do with the artifact mentioned at https://github.com/leanprover/lean4/pull/148.

Kha commented 3 years ago

That sounds like a bug. Could you check and see if you can run the bin/lean executable in https://github.com/leanprover/lean4/suites/3726227515/artifacts/91212300?

benjamin20104 commented 3 years ago

Thanks, that's now working for me.

The version that did not work is the nightly build on 9/8.