## Stream: general

### Topic: local context names

#### 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?

#### Mario Carneiro (Jul 03 2019 at 15:22):

each element in that list is a local_const

#### Mario Carneiro (Jul 03 2019 at 15:22):

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

Thanks!

#### Patrick Massot (Jul 03 2019 at 15:26):

I forgot what expr were...

Last updated: May 11 2021 at 00:31 UTC