## Stream: general

### Topic: environments and parameters

#### Jakob von Raumer (Apr 20 2018 at 13:48):

So I want to emulate inductive types defined in some section with parameters (or variables, I don't care). Can I do that by adding the paramters as local consts to some evironment e and then use e.add_inductive?

#### Simon Hudon (Apr 20 2018 at 13:55):

You would need to make it a proper constant I think. I assume you're writing a user command?

#### Sebastian Ullrich (Apr 20 2018 at 14:00):

There is no list of local consts in an environment, it's all in the parser (unexposed to Lean)

#### Jakob von Raumer (Apr 20 2018 at 14:12):

@Simon Hudon Yes, I am... I'll just take a look at environments...

#### Jakob von Raumer (Apr 20 2018 at 14:13):

@Sebastian Ullrich I don't necessarily need a list of them. So far I get around using parameters by just adding them as parameters to the inductive types I'm constructing and to every function I'm defining.

#### Sebastian Ullrich (Apr 20 2018 at 14:14):

Yes, that's what Lean itself does. It also creates aliases for the applied definitions in the parser, but you can't do that.

#### Jakob von Raumer (Apr 20 2018 at 14:15):

Do you have an idea how to solve that annoyance? Because it really makes my code very messy.

#### Jakob von Raumer (Apr 20 2018 at 14:23):

It sometimes seems a bit arbitrary what's exposed as meta constants and what isn't...

Last updated: May 16 2021 at 05:21 UTC