mathlib
50cdb957
- fix(tactic/suggest): make `library_search` aware of definition of `ne` (#11742)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(tactic/suggest): make `library_search` aware of definition of `ne` (#11742) `library_search` wasn't including results like `¬ a = b` to solve goals like `a ≠ b` and vice-versa. Closes #3428
Author
arthurpaulino
Parents
07735b8a
Loading