diff --git a/frap_book.tex b/frap_book.tex index 39577dc..e89e48c 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -3453,7 +3453,8 @@ In fact, we can prove that any other state is unstuck, though we won't bother he %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\chapter{label{embeddings}Deep Embeddings, Shallow Embeddings, and Options in Between} +\chapter{Deep Embeddings, Shallow Embeddings, and Options in Between} +\label{embeddings} So far, in this book, we have followed the typographic conventions of ordinary mathematics and logic, as they would be worked out on whiteboards. In parallel, we have mechanized all of the definitions and proofs in Coq.