Mathlib v3 is deprecated. Go to Mathlib v4

Def where.select_for_which

Modification history

2020-12-15 17:57
src/tactic/where.lean
ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter (#5330) …
Modified where.select_for_whichView on Github →
2018-12-20 03:40
tactic/where.lean
feat(command): Add `#where` command, dumping environment info (#489) …
Added where.select_for_whichView on Github →