From 21b09b84aa71c68a06a865af37eeae454ef75fba Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 14 Nov 2023 10:29:34 -0500
Subject: [PATCH] update definitions file
---
paper-new/defs.tex | 26 +++++++++++++++++++++++---
1 file changed, 23 insertions(+), 3 deletions(-)
diff --git a/paper-new/defs.tex b/paper-new/defs.tex
index f0b8114..2c54f38 100644
--- a/paper-new/defs.tex
+++ b/paper-new/defs.tex
@@ -7,7 +7,9 @@
\newcommand{\extlc}{\text{Ext-}\lambda}
\newcommand{\extlcm}{\text{Ext-}\lambda^{-\text{trans}}}
\newcommand{\extlcmm}{\text{Ext-}\lambda^{-\text{trans}-\text{cast}}}
+\newcommand{\extlcprime}{\text{Ext-}\lambda'}
\newcommand{\intlc}{\text{Int-}\lambda}
+\newcommand{\intlcbisim}{\text{Int$_\approx$-}\lambda}
\newcommand{\erase}[1]{\lfloor {#1} \rfloor}
@@ -26,6 +28,7 @@
\newcommand{\ra}{\rightharpoonup}
\newcommand{\Ret}[1]{\mathsf{Ret\,}{#1}}
\newcommand{\hole}[1]{\bullet \colon {#1}}
+\newcommand{\dyntodyn}{\dyn \ra\, \dyn}
\newcommand{\up}[2]{\langle{#2}\uarrowl{#1}\rangle}
@@ -36,11 +39,14 @@
\newcommand{\zro}{\textsf{zro}}
\newcommand{\suc}{\textsf{suc}}
\newcommand{\lda}[2]{\lambda {#1} . {#2}}
-\newcommand{\injarr}[1]{\textsf{Inj}_\to ({#1})}
+\newcommand{\injarr}[1]{\textsf{Inj}_\ra ({#1})}
\newcommand{\injnat}[1]{\textsf{Inj}_\text{nat} ({#1})}
\newcommand{\casenat}[4]{\text{Case}_\text{nat} ({#1}) \{ \text{no} \to {#2} \alt \text{nat}({#3}) \to {#4} \}}
-\newcommand{\casearr}[4]{\text{Case}_\to ({#1}) \{ \text{no} \to {#2} \alt \text{fun}({#3}) \to {#4} \}}
+\newcommand{\casearr}[4]{\text{Case}_\ra ({#1}) \{ \text{no} \to {#2} \alt \text{fun}({#3}) \to {#4} \}}
\newcommand{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}
+\newcommand{\matchnat}[4]{\text{match } {#1} \text{ with } \{ \textsf {zero} \Rightarrow {#2} \alt \textsf{ suc } {#3} \Rightarrow {#4} \}}
+
+\newcommand{\refl}{\text{refl}}
\newcommand{\Lift}{\text{Lift}}
@@ -54,10 +60,13 @@
\newcommand{\relcomp}{\odot}
\newcommand{\hasty}[3]{{#1} \vdash {#2} \colon {#3}}
+\newcommand{\vhasty}[3]{{#1} \vdash^v {#2} \colon {#3}}
+\newcommand{\phasty}[3]{{#1} \vdash^p {#2} \colon {#3}}
\newcommand{\etmprec}[4]{{#1} \vdash {#2} \ltdyn_e {#3} \colon {#4}}
\newcommand{\itmprec}[4]{{#1} \vdash {#2} \ltdyn_i {#3} \colon {#4}}
\newcommand{\etmequidyn}[4]{{#1} \vdash {#2} \equidyn_e {#3} \colon {#4}}
\newcommand{\itmequidyn}[4]{{#1} \vdash {#2} \equidyn_i {#3} \colon {#4}}
+\newcommand{\synbisim}{\approx_{\text{syn}}}
\newcommand{\Dwn}{\Downarrow}
\newcommand{\qte}[1]{\text{quote}({#1})}
@@ -82,15 +91,25 @@
\newcommand{\calU}{\mathcal{U}}
\newcommand{\laterhat}{\widehat{\later}}
\newcommand{\El}{\mathsf{El}}
+\newcommand{\Clock}{\mathsf{Clock}}
+
+\newcommand{\Machine}[1]{\mathsf{Machine}\, {#1}}
% Predomains and EP pairs
+\newcommand{\Nat}{\mathsf{Nat}}
\newcommand{\Dyn}{\mathsf{Dyn}}
\newcommand{\ty}[1]{\langle {#1} \rangle}
\newcommand{\li}{L_\mho}
+\newcommand{\liclk}[1]{L_\mho [{#1}]}
+
+\newcommand{\ext}[2]{\text{ext}\,{#1}\,{#2}}
+\newcommand{\map}[2]{\text{map}\,{#1}\,{#2}}
\newcommand{\ltls}{\lesssim}
\newcommand{\bisim}{\approx}
+\newcommand{\semlt}{\le}
+\newcommand{\semltbad}{\lesssim}
%\newcommand{\injarr}{\textsf{Inj}_\to}
%\newcommand{\injnat}{\textsf{Inj}_\mathbb{N}}
@@ -110,4 +129,5 @@
\newcommand{\wrp}{w_r^p}
\newcommand{\wlp}{w_l^p}
-\newcommand{\sem}[1]{\llbracket {#1} \rrbracket}
\ No newline at end of file
+\newcommand{\sem}[1]{\llbracket {#1} \rrbracket}
+\newcommand{\semgl}[1]{{\sem{#1}}^\text{gl}}
\ No newline at end of file
--
GitLab