Commit 2022-11-21 19:57 3536f475

View on Github →

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.

Estimated changes

added def foo1
added def foo2
added def foo3
added def foo4
added def foo5