Commit 2022-11-21 19:57 3536f475

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.