Zulip Chat Archive

Stream: general

Topic: dependencies


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 20 2019 at 21:50):

Short answer is no

view this post on Zulip Mario Carneiro (May 20 2019 at 21:51):

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

view this post on Zulip Rob Lewis (May 20 2019 at 22:10):

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


Last updated: May 14 2021 at 12:18 UTC