# What does x.y notation mean?

In Harper's PFPL (Ed. 2, top of page 8), this notation is used but I don't see a definition. What does $$x.y$$ mean?

This is the notation for Harper's "abstract binding structures": x.t represents the binding site of a variable x and the term t the variable scopes over.
Apparently you are in the parts that define variable bindings. $$\mathcal{B}[\mathcal{X}]_s$$ appears to be the set of terms, or binding structures at sort $$s$$ whose free variables are among $$\mathcal{X}$$. So I would expect (but I don't have the book) that there is in fact an explanation for this notation close by.