Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC