From c33345a4f4b8673fc7a266b77b1d5a2488682d3d Mon Sep 17 00:00:00 2001 From: Vanessa McHale Date: Mon, 30 Apr 2018 05:18:00 -0500 Subject: [PATCH] minor copy edits --- main.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/main.tex b/main.tex index 1e45894..d57ab48 100644 --- a/main.tex +++ b/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