This repository was archived by the owner on Oct 21, 2024. It is now read-only.
Unknown identifier 'take' #215
Description
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.