-
Notifications
You must be signed in to change notification settings - Fork 35
Open
Labels
bugSomething isn't workingSomething isn't working
Description
Describe the bug
https://lean-lang.org/doc/reference/latest/Tactic-Proofs/The-Tactic-Language/#have
In what way is the content incorrect?
Seems like haveI
has been accidentally replaced by another copy of have
Please provide a self-contained Lean example that demonstrates the incorrectness of the statement.
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working