\newcommand{\To}{\Rightarrow}
\newcommand{\inl}{\mathsf{inl}}
\newcommand{\inr}{\mathsf{inr}}
\newcommand{\alt}{\mathrel{\bf \,\mid\,}}


\newcommand{\extlc}{\text{Ext-}\lambda}
\newcommand{\extlcm}{\text{Ext-}\lambda^{-\text{trans}}}
\newcommand{\extlcmm}{\text{Ext-}\lambda^{-\text{trans}-\text{cast}}}
\newcommand{\intlc}{\text{Int-}\lambda}
\newcommand{\erase}[1]{\lfloor {#1} \rfloor}


\newcommand{\uarrowl}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\uarrowr}{\mathrel{\rotatebox[origin=c]{60}{$\leftarrowtail$}}}
\newcommand{\darrowl}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\newcommand{\darrowr}{\mathrel{\rotatebox[origin=c]{120}{$\twoheadleftarrow$}}}
\newcommand{\vuarrow}{\mathrel{\rotatebox[origin=c]{-90}{$\leftarrowtail$}}}
\newcommand{\vdarrow}{\mathrel{\rotatebox[origin=c]{90}{$\twoheadleftarrow$}}}

% Types, terms, and precision 

\newcommand{\dyn}{?}
\newcommand{\nat}{\text{Nat}}
\newcommand{\bool}{\text{Bool}}
\newcommand{\ra}{\rightharpoonup}
\newcommand{\Ret}[1]{\mathsf{Ret\,}{#1}}
\newcommand{\hole}[1]{\bullet \colon {#1}}


\newcommand{\up}[2]{\langle{#2}\uarrowl{#1}\rangle}
\newcommand{\dn}[2]{\langle{#1}\darrowl{#2}\rangle}

\newcommand{\ret}{\mathsf{ret}}
\newcommand{\err}{\mho}
\newcommand{\zro}{\textsf{zro}}
\newcommand{\suc}{\textsf{suc}}
\newcommand{\lda}[2]{\lambda {#1} . {#2}}
\newcommand{\injarr}[1]{\textsf{Inj}_\to ({#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{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}

\newcommand{\Lift}{\text{Lift}}

%\newcommand{\rel}{\circ\hspace{-4px}-\hspace{-4px}\bullet}
\newcommand{\rel}{\mathrel{\circ\mkern-6mu-\mkern-6mu\bullet}}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\gamlt}{\Gamma^\ltdyn}
\newcommand{\deltalt}{\Delta^\ltdyn}
\newcommand{\relcomp}{\odot}

\newcommand{\hasty}[3]{{#1} \vdash {#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{\Dwn}{\Downarrow}
\newcommand{\qte}[1]{\text{quote}({#1})}

% SGDT and Intensional Stuff

\newcommand{\later}{\vartriangleright}
\newcommand{\type}{\texttt{Type}}
\newcommand{\lob}{\text{L\"{o}b}}
\newcommand{\tick}{\mathsf{tick}}
\newcommand{\nxt}{\mathsf{next}}
\newcommand{\fix}{\mathsf{fix}}
\newcommand{\kpa}{\kappa}

% Model-related stuff
\newcommand{\calC}{\mathcal{C}}
\newcommand{\Set}{\mathsf{Set}}
\newcommand{\Yo}{\mathsf{Yo}}
\newcommand{\Hom}{\mathsf{Hom}}
\newcommand{\calS}{\mathcal{S}}
\newcommand{\gfix}{\texttt{gfix}}
\newcommand{\calU}{\mathcal{U}}
\newcommand{\laterhat}{\widehat{\later}}
\newcommand{\El}{\mathsf{El}}


% Predomains and EP pairs
\newcommand{\Dyn}{\mathsf{Dyn}}
\newcommand{\ty}[1]{\langle {#1} \rangle}
\newcommand{\li}{L_\mho}

\newcommand{\ltls}{\lesssim}
\newcommand{\bisim}{\approx}

%\newcommand{\injarr}{\textsf{Inj}_\to}
%\newcommand{\injnat}{\textsf{Inj}_\mathbb{N}}

\newcommand{\id}{\mathsf{id}}
\newcommand{\ep}{\leadsto}

\newcommand{\emb}[2]{\mathsf{emb}_{#1}({#2})}
\newcommand{\proj}[2]{\mathsf{proj}_{#1}({#2})}

\newcommand{\monto}{\to_m}


% Notation for wait functions
\newcommand{\wre}{w_r^e}
\newcommand{\wle}{w_l^e}
\newcommand{\wrp}{w_r^p}
\newcommand{\wlp}{w_l^p}

\newcommand{\sem}[1]{\llbracket {#1} \rrbracket}