From: Francesco Mazzoli <f@mazzo.li>
Date: Mon, 24 Jun 2013 09:33:46 +0000 (+0100)
Subject: ...
X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=6731f090d5edb85f628501e5dcc513e542fce325

...
---

diff --git a/demo.ka b/demo.ka
index 8e9ba5f..60ebdea 100644
--- 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 a1b2419..a2cf6ab 100644
--- 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:
   \[