mathlib
be2038e9 - feat(tactic/expand_exists): parse docstrings, absolute names

Commit

3 years ago

feat(tactic/expand_exists): parse docstrings, absolute names

References

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

Author

0x182d4454fb211940

0x182d4454fb211940

Committer

0x182d4454fb211940

0x182d4454fb211940

Parents

Loading