Zulip Chat Archive

Stream: general

Topic: local context names


view this post on Zulip Patrick Massot (Jul 03 2019 at 15:20):

I have a silly tactic writing question. I know about local_context, which returns a tactic (list expr). But how do you get the names of the local hypotheses?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:22):

each element in that list is a local_const

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:22):

so you can map local_pp_name on the list to get the names

view this post on Zulip Patrick Massot (Jul 03 2019 at 15:25):

Thanks!

view this post on Zulip Patrick Massot (Jul 03 2019 at 15:26):

I forgot what expr were...


Last updated: May 11 2021 at 00:31 UTC