## Stream: general

### Topic: dependencies

#### Rob Lewis (May 20 2019 at 15:01):

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 (May 20 2019 at 15:15):

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

#### Mario Carneiro (May 20 2019 at 21:50):

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