Add RTEquiv to .ott

0xd34df00d · Jan 21, 2021 · b12edfc · b12edfc
1 parent 7edda89
commit b12edfc
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 0 deletions.
diff --git a/tex/common.ott b/tex/common.ott
@@ -7,6 +7,7 @@ terminals :: terminals_ ::=
   | |->     :: :: subst {{ tex \mapsto }}
   | GD		:: :: contextdelta {{ tex \Delta }}
   | ~~>		:: :: evalsto {{ tex \evalsto }}
+  | =trb    :: :: r_equiv {{ tex =_{\tau r\beta} }}
   | in		:: :: in  {{ tex \in }}
   | |-		:: :: proves {{ tex \vdash }}
   | \       :: :: lambda {{ tex \lambda }}

diff --git a/tex/paper.mng b/tex/paper.mng
@@ -385,6 +385,13 @@ with some extra rules for the ADTs and pattern matching.
   \label{fig:surface_opsem}
 \end{figure}
 
+\begin{figure}[ht]
+  \footnotesize
+  \drules[RTEquiv]{$[[ ts1 =trb ts2 ]]$}{type equivalence}{Forward,Backward}
+  \caption{Surface language type equivalence}
+  \label{fig:surface_tyequiv}
+\end{figure}
+
 \begin{figure}[ht]
   \footnotesize
   \drules[TCTX]{$[[ G ok ]]$}{context well-formedness}{Empty,Bind}

diff --git a/tex/surface.ott b/tex/surface.ott
@@ -61,6 +61,16 @@ C {{ tex \nonterm C }} :: logic_ctx_ ::= {{ com logical context }}
 
 defns Jtype :: '' ::=
 
+defn ts1 =trb ts2 :: :: type_r_equiv :: RTEquiv_ {{ com restricted type equivalence }} by
+
+es ~~> es'
+------------------------------------- :: Forward
+[ x |-> es' ] ts =trb [ x |-> es ] ts
+
+es ~~> es'
+------------------------------------- :: Backward
+[ x |-> es ] ts =trb [ x |-> es' ] ts
+
 defn G ok :: :: ctx_wf :: TCTX_ {{ com context well-formedness }} by
 
 -------- :: Empty