Mathlib v3 is deprecated. Go to Mathlib v4

Def where.inflate

Modification history

2020-04-21 17:16
src/tactic/where.lean
fix(tactic/where): remove hackery from `#where`, using Lean 3c APIs (#2465) …
Deleted where.inflateView on Github →
2018-12-20 03:40
tactic/where.lean
feat(command): Add `#where` command, dumping environment info (#489) …
Added where.inflateView on Github →