Zulip Chat Archive

Stream: general

Topic: environments and parameters


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Jakob von Raumer (Apr 20 2018 at 14:12):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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