curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

Commit
d873288e25d7e09f220f8b48bde92434834b2357
Parent
a22455165c62b855fb032a701989bf1f68cc7013
Author
Pablo <pablo-escobar@riseup.net>
Date

Changed the pauses

Diffstat

1 file changed, 7 insertions, 7 deletions

Status File Name N° Changes Insertions Deletions
Modified main.tex 14 7 7 
diff --git a/main.tex b/main.tex
@@ -1,4 +1,4 @@
-\def\hidepauses{yes}
+%\def\hidepauses{yes}
 \input{preamble}
 
 \definecolor{hacker}{RGB}{4,165,90}
@@ -22,8 +22,6 @@
 
       \pause
 
-      \pause
-
     \item Dedução natural\dots
       \[
         \begin{array}{cc}
@@ -384,6 +382,8 @@
     \end{column}
   \end{columns}
 
+  \pause
+
   \begin{figure}
     \centering
     \inputminted{lean}{examples/liquid.lean}
@@ -405,17 +405,17 @@
           \begin{itemize}
             \item<5-> Classificação dos grupos simples finitos
 
-            \item<6-> A prova de Mochizuki da conjetura abc
+            \item<5-> A prova de Mochizuki da conjetura abc
 
-            \item<7-> A prova de Hales da conjectura de Kepler de 2015!
+            \item<6-> A prova de Hales da conjectura de Kepler de 2015!
 
-            \item<8->
+            \item<6->
               A conclusão do
               \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
               Tensor Experiment}} em julho de 2022!
           \end{itemize}
 
-        \item<9-> \emph{Who watches the Watchmen?}
+        \item<7-> \emph{Who watches the Watchmen?}
           \includegraphics[height=1em]{images/watchmen.eps}
       \end{itemize}
     \end{column}