The Subst Γ Δ notation from the Substitution appendix is a great notation, but the Confluence chapter uses it without providing a definition, explanation, or forward reference. It warrants a word, I think.
Ultimately I think the book would be improved by introducing this notation in the DeBruijn chapter.
The
Subst Γ Δnotation from the Substitution appendix is a great notation, but the Confluence chapter uses it without providing a definition, explanation, or forward reference. It warrants a word, I think.Ultimately I think the book would be improved by introducing this notation in the DeBruijn chapter.