diff options
| -rw-r--r-- | demo.ka | 23 | ||||
| -rw-r--r-- | presentation.tex | 9 |
2 files changed, 8 insertions, 24 deletions
@@ -12,30 +12,11 @@ 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: \[ |