mathlib
46abb216 - feat(tactic/expand_exists): replace syntax with proposed list syntax

Commit

3 years ago

feat(tactic/expand_exists): replace syntax with proposed list syntax

References

expand_exists_improvements

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

Author

0x182d4454fb211940

0x182d4454fb211940

Committer

0x182d4454fb211940

0x182d4454fb211940

Parents

Loading