projects
/
bitonic-mengthesis.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
...
[bitonic-mengthesis.git]
/
presentation.tex
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}