update definitions file

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