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

...
---

diff --git a/presentation.tex b/presentation.tex
index a2cf6ab..a8e4995 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -231,8 +231,8 @@
   \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.
@@ -374,7 +374,7 @@
   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}