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

Open

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

0x182d4454fb211940 wants to merge 6 commits into master from expand_exists_improvements

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

be2038e9

feat(tactic/expand_exists): apply parsed arguments

715a24f1

test(tactic/expand_exists): add tests for docstring and namespaces

0154d673

doc(tactic/expand_exists): document namespace & docstring

1c81d260

robertylewis commented on 2022-07-28

robertylewis added awaiting-author

robertylewis added t-meta

robertylewis added modifies-tactic-syntax

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

f7efac2f

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

46abb216

robertylewis assigned

robertylewis 3 years ago

kim-em added too-late

eric-wieser requested a review 2 years ago

Reviewers

robertylewis

eric-wieser

digama0

Assignees

robertylewis

Labels

awaiting-author t-meta modifies-tactic-syntax too-late

Milestone

No milestone