Zulip Chat Archive
Stream: general
Topic: context like expr lists?
Jakob von Raumer (Mar 13 2018 at 13:24):
How do I construct a list of expressions where later entries can depend on earlier ones? Like (A : Sort u) (a : A) as a minimal example... Do I have to use local constants?
Mario Carneiro (Mar 13 2018 at 13:25):
when you say list of expressions, are you working in meta land?
Jakob von Raumer (Mar 13 2018 at 13:25):
Yes
Mario Carneiro (Mar 13 2018 at 13:26):
it's just list expr
Mario Carneiro (Mar 13 2018 at 13:26):
all that binding stuff is handled by you
Jakob von Raumer (Mar 13 2018 at 13:26):
Yes, but how is the above example represented for example?
Mario Carneiro (Mar 13 2018 at 13:27):
the first expr is `(Sort u), the second is either `(A) or #0 depending on whether A is in context
Jakob von Raumer (Mar 13 2018 at 13:31):
Well at the time I define the list, A is clearly not in context, right?
Mario Carneiro (Mar 13 2018 at 13:31):
Maybe; perhaps you are planning for when it is. What's your use case?
Jakob von Raumer (Mar 13 2018 at 13:32):
Just experimenting with the add_inductive API a bit... which is where it should be used as list of parameters or such
Jakob von Raumer (Mar 13 2018 at 13:33):
And meta example : list expr := [\(Sort 1), \`(A)]` immediately gives me "unknown identifier A"..
Jakob von Raumer (Mar 13 2018 at 13:33):
sigh How do I escape backticks here?
Mario Carneiro (Mar 13 2018 at 13:34):
add_inductive doesn't take a list of parameters, it takes ty : expr that specifies the whole type
Mario Carneiro (Mar 13 2018 at 13:34):
Since it's a single expression, all the binding is done via expr.pi, and dependencies are done with var (de bruijn variables)
Mario Carneiro (Mar 13 2018 at 13:35):
That is, ty should be a closed term
Mario Carneiro (Mar 13 2018 at 13:37):
escape backticks with more backticks `` `escaped` ``
Jakob von Raumer (Mar 13 2018 at 13:37):
But it takes a list of constructtors, right?
Mario Carneiro (Mar 13 2018 at 13:37):
The constructor types are also closed terms
Mario Carneiro (Mar 13 2018 at 13:37):
they repeat all the parameters, with the same types
Jakob von Raumer (Mar 13 2018 at 13:38):
Hm, I'd still like to have a data structure like that...
Mario Carneiro (Mar 13 2018 at 13:38):
(this is done because constructors may change the binding type, like making things implicit)
Mario Carneiro (Mar 13 2018 at 13:38):
Usually, we work in a context, and then it's a list expr
Mario Carneiro (Mar 13 2018 at 13:39):
the whole tactic state is built around that
Mario Carneiro (Mar 13 2018 at 13:39):
that's where local constants come in
Jakob von Raumer (Mar 13 2018 at 13:40):
expr could use a bit more documentation somehow, it's really hard to figure out what local constants are
Kevin Buzzard (Mar 13 2018 at 13:56):
@Jakob von Raumer Write what you know and PR it to mathlib/docs/
Kevin Buzzard (Mar 13 2018 at 13:56):
and then ask about what you don't know
Kevin Buzzard (Mar 13 2018 at 13:57):
we're trying to make some community-based docs in there
Kevin Buzzard (Mar 13 2018 at 13:57):
informal and hopefully useful
Jakob von Raumer (Mar 13 2018 at 13:57):
I'll try :)
Kevin Buzzard (Mar 13 2018 at 13:58):
The rule I usually go for is "if it's not in the reference manual, and it's either not in TPIL/Programming In Lean or it's hard to find, then stick it in mathlib/docs"
Jakob von Raumer (Mar 13 2018 at 13:59):
I think it should be in PIL but it's noted as a TODO there
Kevin Buzzard (Mar 13 2018 at 14:00):
Then I would urge you to create a short text file called expr.md and simply write some background and then what you're stuck on and PR it to that docs dir. You can assume people have read PIL.
Jakob von Raumer (Mar 14 2018 at 15:09):
What is the purpose of the second name argument to expr.local_const?
Jakob von Raumer (Mar 14 2018 at 15:10):
Ah, got it, pretty printer name...
Last updated: Dec 20 2023 at 11:08 UTC