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