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:
6731f09
)
...
author
Francesco Mazzoli
<f@mazzo.li>
Mon, 24 Jun 2013 12:29:16 +0000
(13:29 +0100)
committer
Francesco Mazzoli
<f@mazzo.li>
Mon, 24 Jun 2013 12:29:16 +0000
(13:29 +0100)
presentation.tex
patch
|
blob
|
history
diff --git
a/presentation.tex
b/presentation.tex
index a2cf6aba85c816091641715567119ec7903063ac..a8e4995d7a36b8314c159f2c5364d2e2ebe5721d 100644
(file)
--- a/
presentation.tex
+++ b/
presentation.tex
@@
-231,8
+231,8
@@
\mykant\ is an \emph{interactive theorem prover}/\emph{functional
programming language}, 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
in the tradition of Agda and Epigram (and to a lesser extent
+
Coq), but with a more powerful notion
of \emph{equality}.
We have figured out theory of \mykant, and have a near-complete
implementation.
We have figured out theory of \mykant, and have a near-complete
implementation.
@@
-374,7
+374,7
@@
Or
\[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \]
Or
\[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \]
- Yes: to typecheck, we reduce terms fully (to their \emph{normal
} form
)
+ Yes: to typecheck, we reduce terms fully (to their \emph{normal
form}
)
before comparing:
\[
\begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
before comparing:
\[
\begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}