mathlib3
5b5b432e - fix(tactic/tfae): remove unused arg in tfae_have (#8727)

Commit
4 years ago
fix(tactic/tfae): remove unused arg in tfae_have (#8727) Since this "discharger" argument is not using the interactive tactic parser, you can only give names of tactics here, and in any case it's unused by the body, so there is no point in specifying the discharger in the first place.
Author
Parents
Loading