search

leanprover / tutorial

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

Unknown identifier 'take' #215

Open jachymb opened 3 years ago

jachymb commented 3 years ago

The first "Try it yourself example" of the chapter "4 Quantifiers and Equality" won't compile and throws the error Unknown identifier 'take' using Lean 3.28. I guess there should be an assume instead of take and also take probably should not be hilighted anymore and have it's other mentions in the document removed too.

jachymb commented 3 years ago

but it seems the tutorial is intended for LEAN 2 only? So maybe this should just be closed.