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

Open

Commits

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

0x182d4454fb211940 committed 3 years ago
feat(tactic/expand_exists): apply parsed arguments

0x182d4454fb211940 committed 3 years ago
test(tactic/expand_exists): add tests for docstring and namespaces

0x182d4454fb211940 committed 3 years ago
doc(tactic/expand_exists): document namespace & docstring

0x182d4454fb211940 committed 3 years ago
feat(tactic/expand_exists): use `_root_` instead of `@`

0x182d4454fb211940 committed 3 years ago
feat(tactic/expand_exists): replace syntax with proposed list syntax

0x182d4454fb211940 committed 3 years ago