From bc20b219d90c3128a42cea7f6124dd9a1c7c6085 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 7 Jan 2020 12:42:21 -0500
Subject: [PATCH] Revert "start adding recursive value types"
This reverts commit 528a54c6958363c26d339baf347132b7e8d44a3d.
---
paper/gtt.tex | 8 ++------
1 file changed, 2 insertions(+), 6 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 117cafa..d9c6f24 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1045,8 +1045,8 @@ orderings on types and terms.
\[
\begin{array}{l}
\begin{array}{rl|rl}
- A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 & X \mid \mu X. A
- \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B \mid \u Y \mid \u \nu \u Y. \u B\\
+ A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 &
+ \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
V ::= & \begin{array}{l}
\colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V} \\
@@ -1502,10 +1502,6 @@ in the domain~\citep{newahmed18,newlicata2018-fscd}.
\begin{mathpar}
\framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
-
- \inferrule{}{A[\mu X.A/X] \ltdyn \mu X. A}
-
- \inferrule{A[A'/X] \ltdyn A'}{\mu X. A \ltdyn A'}
\inferrule*[lab=VTyRefl]{ }{A \ltdyn A}
--
GitLab