search

leanprover / tutorial

Lean Tutorials
https://leanprover.github.io/tutorial
Apache License 2.0
43 stars 46 forks source link

fix(04,08,11,13): fix chapters to reflect changes in Lean. Closes #196. #197

Closed avigad closed 8 years ago

avigad commented 8 years ago

This fix adapts to recent changes in Lean, notably the removal of by+, assert, etc.

The tutorial needs an overhaul, and I have a list of corrections Nathan Carter that is now almost a year old. But at this point it seems to make sense to wait for Lean 3, and revise the tutorial for the new system.

@leodemoura I am not sure what to say about the semicolon in tactic mode. You removed backtracking, right? So is there any difference between by foo; bar and begin foo, bar end?

avigad commented 8 years ago

@soonhokong My bad. I just added that fix. Now "make test" and "make" both succeed, so hopefully we're good.

soonhokong commented 8 years ago

@avigad, thanks! I'll close this issue and process other PRs tonight.

leodemoura commented 8 years ago

@leodemoura I am not sure what to say about the semicolon in tactic mode. You removed backtracking, right? So is there any difference between by foo; bar and begin foo, bar end?

The master branch still implements backtracking. So, this part is fine for now. After the refactoring, and lean3 becomes the main branch, we will need a major change in the tactic section. We will use the monadic do notation (like Haskell) for writing tactic scripts. I'm planning to keep the begin - end blocks for "interactive use". The main difference will be implicit quotation, and ,-notation for entering a sequence of tactics.

avigad commented 8 years ago

I'm looking forward to the new tactic language.

Something caused at least one of these two examples in the tutorial to break (I think it was the second one): https://github.com/leanprover/tutorial/pull/197/commits/0fdeb02848f48f4857e28eff74596952b14b227e#diff-77be5851357653823680ddcaf7d93760R258

So I commented out the section. I think we can do without it.