From bfb8210faf4c1ad940a5c4ecd61c7ba3bdc1addf Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Fri, 19 Jan 2024 14:44:09 -0500
Subject: [PATCH] add some definitions
---
paper-new/defs.tex | 15 +++++++++++++--
1 file changed, 13 insertions(+), 2 deletions(-)
diff --git a/paper-new/defs.tex b/paper-new/defs.tex
index 11cabf1..e4df2f2 100644
--- a/paper-new/defs.tex
+++ b/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
--
GitLab