mathlib
f7efac2f - feat(tactic/expand_exists): use `_root_` instead of `@`

Commit

3 years ago

feat(tactic/expand_exists): use `_root_` instead of `@`

References

#15732 - feat(tactic/expand_exists): create in namespace & docstring

Author

0x182d4454fb211940

0x182d4454fb211940

Parents

Loading