diff -r 94db2636a296 -r 7af4e2420a8c ChengsongTanPhdThesis/Chapters/Inj.tex --- a/ChengsongTanPhdThesis/Chapters/Inj.tex Tue Nov 22 12:50:04 2022 +0000 +++ b/ChengsongTanPhdThesis/Chapters/Inj.tex Sat Nov 26 16:18:10 2022 +0000 @@ -698,7 +698,7 @@ to indicate that a value $v$ could be generated from a lexing algorithm with input $r$. They call it the value inhabitation relation, defined by the rules. -\begin{figure}[H]\label{fig:inhab} +\begin{figure}[H] \begin{mathpar} \inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em} @@ -712,7 +712,7 @@ \inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars \; vs : r^*} \end{mathpar} -\caption{The inhabitation relation for values and regular expressions} +\caption{The inhabitation relation for values and regular expressions}\label{fig:inhab} \end{figure} \noindent The condition $|v| \neq []$ in the premise of star's rule