Document notation #630
Document notation #630
Conversation
book/src/glossary.md
Outdated
| | `^0`, `^1.0` | [Bound variable] | | ||
| | `!0` | [Placeholder] | |
There was a problem hiding this comment.
I have to say that this notation confuses me a bit; I just copied this part from the issue, so I would appreciate if someone more knowledgeable could double-check this :)
There was a problem hiding this comment.
These look right. If these confuse you though, they most certainly confuse someone else. So, what confuses you?
There was a problem hiding this comment.
Well, for one the syntax confuses me: what does 1.0 mean? It looks a floating point number, which I'm not used to seeing to represent a variable. I think it's a de Bruijn index, but I still don't fully understand it.
Also, I don't understand the difference between a placeholder and a bound variable/inference variable; the docs for it don't explicitly describe the difference.
There was a problem hiding this comment.
Yeah, so maybe it's worth describing the syntax here a bit. I'll describe a little bit here. I'm not quite sure the best place to put this though. (Or how much might be duplicated from other places in the book)
Inference variables have the format ?0. This means that in the current inference context, this is variable 0.
Bound variables can take the format of ^1.0 or ^0. In the former case, the 1 represents the Debruijn index of the variable. The 0 represents the index in that level of binding. For example, in forall<X,Y> { forall <Z> { X } }, X could be represented as ^1.0. If the Debruijn index is 0, then it may sometimes be omitted, leading the the second format ^0.
Placeholders take the format !1_0 or !0. For the former, the 1 is universe index of the placeholder whereas the 0 is the index in that universe. If the universe is 0, then it can be omitted, leading to the second format.
I'm not sure if this is the right place to explain placeholders vs bound or inference vars. I would have to think of a good explanation anyways. Let's just focus on notation here, for now.
There was a problem hiding this comment.
Thanks for the description! I'll add some of that to the docs.
There was a problem hiding this comment.
What's an example of a rule where a placeholder would be created?
camelid
force-pushed
the
notation-docs
branch
from
2187b0d to
dfe2659
Compare
|
Not sure why CI is failing... EDIT: It looks like it's partially because of #629. |
camelid
force-pushed
the
notation-docs
branch
from
037058a to
fe18075
Compare
|
Looks like |
|
So, looks like a bunch of stuff in I think the |
camelid
force-pushed
the
notation-docs
branch
from
ae98d90 to
5722439
Compare
* Fix formatting * Use `notrust` for code blocks with invalid Rust syntax * Use Unicode instead of LaTeX (LaTeX isn't supported)
camelid
force-pushed
the
notation-docs
branch
from
5722439 to
ef3b576
Compare
|
Okay, CI should pass now! (except for linkcheck) |
|
@bors r+ |
|
📌 Commit ef3b576 has been approved by |
|
☀️ Test successful - checks-actions |
Fixes #561.