mathlib

dff8393c - feat(tactic/lint): add unprintable tactic linter (#11725)

feat(tactic/lint): add unprintable tactic linter (#11725) This linter will banish the recurring issue of tactics for which `param_desc` fails, leaving a nasty error message in hovers. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>