minor copy edits

main.tex

@@ -787,7 +787,7 @@
 
 %We define for Plutus Core a number of typing judgments which explain ways that a program can be well-formed. First, in Figure \ref{fig:Plutus_core_contexts}, we define the grammar of the various kinds of contexts that these judgments hold under. Nominal contexts contain information about the various declared names that exist within the system --- module names, exported types, exported terms, and then term names and their definitions, term constructors, type constructors, and type names and their definitions.
 
-%We refer to the components of a nominal context by dotted names ($\Theta.\repetition{l}$, $\Theta.\repetition{\metaqualtycon{}|\metaqualtyname{}}$, $\Theta.\repetition{\metaqualcon{}|\metaqualname{}}$, and $\Theta.\repetition{nj}$). Variable contexts contain information about the nature of variables --- type variables with their kind, and term variables with their type. The overall context $\Theta$ consists of nominal and variable contexts, along with the name of the current module being elaborated and the name of imported modules. As with nominal contexts, we also refer to these by dotted names ($\Theta.l$, $\Theta.\repetition{l}$, $\Theta.\Delta$, and $\Theta.\Gamma$) In the inference rules, we use \(\Theta, \typeJ{\alpha}{K}\) to mean $\Theta$ with it's variable context $\Gamma$ extended with $\typeJ{\alpha}{K}$, and \(\Theta, \termJ{x}{A}\) to mean $\Theta$ with it's variable context $\Gamma$ extended with $\termJ{x}{A}$.
+%We refer to the components of a nominal context by dotted names ($\Theta.\repetition{l}$, $\Theta.\repetition{\metaqualtycon{}|\metaqualtyname{}}$, $\Theta.\repetition{\metaqualcon{}|\metaqualname{}}$, and $\Theta.\repetition{nj}$). Variable contexts contain information about the nature of variables --- type variables with their kind, and term variables with their type. The overall context $\Theta$ consists of nominal and variable contexts, along with the name of the current module being elaborated and the name of imported modules. As with nominal contexts, we also refer to these by dotted names ($\Theta.l$, $\Theta.\repetition{l}$, $\Theta.\Delta$, and $\Theta.\Gamma$) In the inference rules, we use \(\Theta, \typeJ{\alpha}{K}\) to mean $\Theta$ with its variable context $\Gamma$ extended with $\typeJ{\alpha}{K}$, and \(\Theta, \termJ{x}{A}\) to mean $\Theta$ with its variable context $\Gamma$ extended with $\termJ{x}{A}$.
 
 %Then, in Figure \ref{fig:Plutus_core_type_well_formedness}, we define what it means for a type construct to inhabit a kind. Plutus Core is a higher-kinded version of System-F with constructors and some primitive types, so we have a number of standard System-F rules together with some obvious extensions