Commit 2019-08-30 16:13 2db7fa45

feat(sanity_check): improve sanity_check (#1369)

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.