dependencies

Stream: general

[Rob Lewis]

We don't have a tactic version of #print axioms f, do we? Or any way to check whether a declaration depends on sorry?

[Jesse Michael Han]

there's meta constant is_sorry in expr.lean, but that's only a basic ingredient of what you want

[Mario Carneiro]

Short answer is no

[Mario Carneiro]

It can be done in the tactic framework though (at significant cost)

[Rob Lewis]

I was hoping to find a way to hack it with emit_command_here but I don't think it's doable.