projects
/
bitonic-mengthesis.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
ec1119d
)
...
author
Francesco Mazzoli
<f@mazzo.li>
Mon, 24 Jun 2013 09:33:46 +0000
(10:33 +0100)
committer
Francesco Mazzoli
<f@mazzo.li>
Mon, 24 Jun 2013 09:33:46 +0000
(10:33 +0100)
demo.ka
patch
|
blob
|
history
presentation.tex
patch
|
blob
|
history
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 }
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)
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?}
\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}.
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}
\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}}
\]
\[
\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:
\[
Instead, we have a hierarchy:
\[