mathlib
0154d673
- test(tactic/expand_exists): add tests for docstring and namespaces
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
test(tactic/expand_exists): add tests for docstring and namespaces
References
#15732 - feat(tactic/expand_exists): create in namespace & docstring
Author
0x182d4454fb211940
Committer
0x182d4454fb211940
Parents
715a24f1
Loading