environments and parameters

Stream: general

[Jakob von Raumer]

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]

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

[Sebastian Ullrich]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

@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]

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]

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

[Jakob von Raumer]

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