add some definitions

paper-new/defs.tex

@@ -40,7 +40,7 @@
 \newcommand{\dnc}[2]{\text{dn}\,{#1}\,{#2}}
 
 
-\newcommand{\ret}{\mathsf{ret}}
+% \newcommand{\ret}{\mathsf{ret}}
 \newcommand{\err}{\mho}
 \newcommand{\zro}{\textsf{zro}}
 \newcommand{\suc}{\textsf{suc}}
@@ -50,7 +50,7 @@
 \newcommand{\casenat}[4]{\text{Case}_\text{nat} ({#1}) \{ \text{no} \to {#2} \alt \text{nat}({#3}) \to {#4} \}}
 \newcommand{\casearr}[4]{\text{Case}_\ra ({#1}) \{ \text{no} \to {#2} \alt \text{fun}({#3}) \to {#4} \}}
 \newcommand{\casedyn}[5]{\text{Case}_\Dyn ({#1}) \{ \text{nat}({#2}) \to {#3} \alt \text{fun}({#4}) \to {#5} \}}
-\newcommand{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}
+%\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}}
@@ -174,6 +174,11 @@
 \newcommand{\ptbv}{\text{ptb}^\mathcal{V}}
 \newcommand{\ptbe}{\text{ptb}^\mathcal{E}}
 
+\newcommand{\Ppure}{P}
+\newcommand{\Pk}{P^K}
+\newcommand{\ptbk}{\text{ptb}^K}
+
+
 \newcommand{\upf}{\text{up}}
 \newcommand{\dnf}{\text{dn}
 }
@@ -218,3 +223,9 @@
 
 
 \newcommand{\da}{\downarrow}
+
+\newcommand{\ret}{\text{ret}}
+\newcommand{\bind}[3]{{#1} <- {#2}\, ; \, {#3}}
+
+\newcommand{\piv}{\Pi^\mathcal{V}}
+\newcommand{\pie}{\Pi^\mathcal{E}}
\ No newline at end of file