tutorial icon indicating copy to clipboard operation
tutorial copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Unknown identifier 'take'

Open jachymb opened this issue 3 years ago • 1 comments

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 avatar Apr 10 '21 20:04 jachymb

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

jachymb avatar Apr 10 '21 20:04 jachymb