starting the missing chapter

MevenBertrand · May 12, 2022 · 8ee21af · 8ee21af
1 parent 65327b8
commit 8ee21af
Show file tree

Hide file tree

Showing 3 changed files with 521 additions and 20 deletions.
diff --git a/Manuscript/main.tex b/Manuscript/main.tex
@@ -36,7 +36,7 @@
 \usepackage{styles/macros}
 \usepackage{styles/alectryon-minted}
 
-% \includeonly{technical-intro}
+\includeonly{typed-untyped-algo}
 
 \graphicspath{{./figures/}} % Paths where images are looked for
 

diff --git a/Manuscript/styles/macros.sty b/Manuscript/styles/macros.sty
@@ -402,4 +402,44 @@ set fill color=DarkRed!10,
 ch/.style={
 set fill color=DarkBlue!10,
 }
-}
+}
+
+% Bidirectional conversion
+
+\knowledgenewrobustcmd{\bconvop}{\mathrel{\cmdkl{\cong}}}
+\knowledgenewrobustcmd{\convhop}{\mathrel{\cmdkl{\cong_{\symup{h}}}}}
+\knowledgenewrobustcmd{\bcumop}{\mathrel{\cmdkl{\preceq}}}
+\knowledgenewrobustcmd{\cumhop}{\mathrel{\cmdkl{\preceq_{\symup{h}}}}}
+\knowledgenewrobustcmd{\nconvop}{\mathrel{\cmdkl{\approx}}}
+% \knowledgenewrobustcmd{\nconvhop}{\mathrel{\cmdkl{\approx_{\symup{h}}}}}
+
+\NewDocumentCommand{\bconv}{m m m o}
+	{#1 \vdash #2 \bconvop #3 \cty \IfValueT{#4}{#4}}
+\NewDocumentCommand{\convh}{m m m o}
+  {#1 \vdash #2 \convhop #3 \cty \IfValueT{#4}{#4}}
+\NewDocumentCommand{\bcum}{m m m}
+	{#1 \vdash #2 \bcumop #3 \cty}
+\NewDocumentCommand{\cumh}{m m m}
+  {#1 \vdash #2 \cumhop #3 \cty}
+\newcommand{\nconv}[4]{#1 \vdash #2 \nconvop #3 \ity #4}
+\newcommand{\pnconv}[5]{#2 \vdash #3 \nconvop #4 \pity{#1} #5}
+
+% \NewDocumentCommand{\buconv}{m m m}
+% 	{#1 \vdash #2 \bconvop #3}
+% \NewDocumentCommand{\uconvh}{m m m}
+%   {#1 \vdash #2 \convhop #3}
+% \NewDocumentCommand{\bucum}{m m m}
+% 	{#1 \vdash #2 \bcumop #3}
+% \NewDocumentCommand{\ucumh}{m m m}
+%   {#1 \vdash #2 \cumhop #3}
+% \newcommand{\nuconv}[3]{#1 \vdash #2 \nconvop #3}
+
+\NewDocumentCommand{\buconv}{m m m}
+	{#2 \bconvop #3}
+\NewDocumentCommand{\uconvh}{m m m}
+  {#2 \convhop #3}
+\NewDocumentCommand{\bucum}{m m m}
+	{#2 \bcumop #3}
+\NewDocumentCommand{\ucumh}{m m m}
+  {#2 \cumhop #3}
+\newcommand{\nuconv}[3]{#2 \nconvop #3}