diff --git a/main.tex b/main.tex
@@ -85,7 +85,7 @@
\inputminted{python}{examples/exhaustion.py}
\end{figure}
\end{itemize}
-
+
\pause
\begin{theorem}[Conjectura de Kepler]
@@ -95,7 +95,7 @@
\begin{itemize}
\item Provado em 1998 por Thomas Hales via exaustão
-
+
\pause
\item E se o número de casos não for finito???
@@ -152,7 +152,7 @@
\begin{figure}
\centering
\begin{tabular}{|l|l|}
- \hline
+ \hline
Termos
& Fórmulas \\
\hline
@@ -186,7 +186,7 @@
\inputminted{python}{examples/fake-theorem.py}
\end{column}
\end{columns}
-
+
\pause
\begin{align*}
@@ -197,7 +197,7 @@
0 & \text{caso contrário} \\
\end{cases}
\end{align*}
-
+
\pause
\begin{itemize}
@@ -215,29 +215,29 @@
\begin{frame}{A Correspondência de Curry-Howard}
\begin{center}
\begin{tabular}{rcl}
- Provar que vale \(A\)
- & \(\leftrightsquigarrow\)
+ Provar que vale \(A\)
+ & \(\leftrightsquigarrow\)
& Encontrar \(a \in \{ \text{provas de}\ A\}\)
\end{tabular}
\end{center}
-
+
\pause
\begin{itemize}
- \item Proposições como tipos
+ \item Proposições como tipos
\begin{center}
\begin{tabular}{rcl}
- \(A\)
- & \(\leftrightsquigarrow\)
+ \(A\)
+ & \(\leftrightsquigarrow\)
& \(\{\text{provas de}\ A \}\) \\
- \(A\ \text{e}\ B\)
- & \(\leftrightsquigarrow\)
+ \(A\ \text{e}\ B\)
+ & \(\leftrightsquigarrow\)
& \(\{\text{provas de}\ A \} \times \{\text{provas de}\ B \}\) \\
- \(A\ \text{ou}\ B\)
- & \(\leftrightsquigarrow\)
+ \(A\ \text{ou}\ B\)
+ & \(\leftrightsquigarrow\)
& \(\{\text{provas de}\ A \} \cup \{\text{provas de}\ B \}\) \\
\(A \implies B\)
- & \(\leftrightsquigarrow\)
+ & \(\leftrightsquigarrow\)
& \(\{\text{provas de}\ A \} \to \{\text{provas de}\ B \}\) \\
\end{tabular}
\end{center}
@@ -265,11 +265,11 @@
\begin{center}
\begin{tabular}{rcl}
- Provar que vale \(A\)
- & \(\leftrightsquigarrow\)
+ Provar que vale \(A\)
+ & \(\leftrightsquigarrow\)
& Construir \(a : \{ \text{provas de}\ A\}\) \\
Checar a prova
- & \(\leftrightsquigarrow\)
+ & \(\leftrightsquigarrow\)
& Checar os tipos
\end{tabular}
\end{center}