...

diff --git a/demo.ka b/demo.ka
index 8e9ba5ffda44fbdc76b8f71ef18d7817c4396b2c..60ebdeaa5463c0966cfba8c1fd890c2a6eefca30 100644 (file)
--- a/demo.ka
+++ b/demo.ka
@@ -11,31 +11,12 @@ data Nat : * ⇒ { zero : Nat | suc : Nat → Nat }
 data List : [A : *] → * ⇒
   { nil : List A | cons : A → List A → List A }
 
-nonEmpty [A : *] [l : List A] : * ⇒ (
-   {| h1 |}
-)
-
-nonEmpty [A : *] [l : List A] : * ⇒ (
-  List-Elim l (λ _ ⇒ *) {|h1|} {|h2|}
-)
-
 nonEmpty [A : *] [l : List A] : * ⇒ (
   List-Elim l (λ _ ⇒ *) Empty (λ _ _ _ ⇒ Unit)
 )
 
 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
   List-Elim l (λ l ⇒ nonEmpty A l → A)
-    {|h1|} {|h2|}
-)
-
-head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
-  List-Elim l (λ l ⇒ nonEmpty A l → A)
-   (λ p ⇒ {|h1 p|})
-   (λ x l pl pxl ⇒ {|h2 x l pl pxl|})
-)
-
-head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
-  List-Elim l (λ l ⇒ nonEmpty A l → A)
-    (λ p ⇒ absurd A p)
-    (λ x l pl pxl ⇒ x)
+    {| h1 |}
+    {| h2 |}
 )

diff --git a/presentation.tex b/presentation.tex
index a1b2419ca7bc50da5bb4739d1f0d54e704a1d8a5..a2cf6aba85c816091641715567119ec7903063ac 100644 (file)
--- a/presentation.tex
+++ b/presentation.tex
@@ -228,11 +228,14 @@
 \begin{frame}
   \frametitle{\mykant?}
 
-  \mykant\ is an \emph{interactive theorem prover}, implemented in
-  Haskell.
+  \mykant\ is an \emph{interactive theorem prover}/\emph{functional
+    programming language}, implemented in Haskell.
 
   It is similar in scope to Agda or Coq, but with a more powerful notion
   of \emph{equality}.
+
+  We have figured out theory of \mykant, and have a near-complete
+  implementation.
 \end{frame}
 
 \begin{frame}
@@ -532,7 +535,7 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   \[
   \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
   \]
-  Much like na{\"i}ve set theory is (Girard's paradox).
+  Similar to Russel's paradox in na{\"i}ve set theory.
 
   Instead, we have a hierarchy:
   \[