mathlib

3536f475 - feat(tactic/print_sorry): add `#print_sorry_in` command (#16911)

feat(tactic/print_sorry): add `#print_sorry_in` command (#16911) Note: This command will happily print internal declarations like `foo._proof_i`. You could make it a bit nicer by not printing these as separate declarations, but the current version is already very useful, and I don't want to spend too much time on Lean 3 metaprogramming.