mathlib3
ea7e3ff7 - feat(tactic/cache): allow optional := in haveI (#8631)

Commit
4 years ago
feat(tactic/cache): allow optional := in haveI (#8631) This syntactic restriction was originally added because it was not possible to reset the instance cache only for a given goal. This limitation has since been lifted (a while ago, I think), and so the syntax can be made more like `have` now.
Author
Parents
Loading