mathlib

2db7fa45 - feat(sanity_check): improve sanity_check (#1369)

feat(sanity_check): improve sanity_check (#1369) * feat(sanity_check): improve sanity_check - add hole command for sanity check (note: hole commands only work when an expression is expected, not when a command is expected, which is unfortunate) - print the type of the unused arguments - print whether an unused argument is a duplicate - better check to filter automatically generated declarations - do not print arguments of type `parse _` - The binding brackets from `tactic.where` are moved to `meta.expr`. The definition is changed so that strict implicit arguments are printed as `{{ ... }}` * typos * improve docstring * Also check for duplicated namespaces Fun fact: I had to remove an unused argument from `decidable_chain'` for my function to work.