Correct disjunction example

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4

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

Apache License 2.0

164 stars 93 forks source link

Correct disjunction example #20

Closed Lehnart closed 3 years ago

Lehnart commented 3 years ago

Hey,

Just a quick fix on 1st example for disjunction which isn't working with lean-4.0.0-m2. Notice that the next examples aren't working either but I don't know how to correct them for now.

Lehnart commented 3 years ago

I saw somewhere else that I should use the nightly to make it work. I just close the pull request to try it out.