Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-20 03:40 caa20760

View on Github →

feat(command): Add #where command, dumping environment info (#489) The command tells you your current namespace (wherever you write it), the current includes, and the current variables which have been used at least once.

Estimated changes