From 77835ae8b245290c8e9593bf504e4ffc267154fe Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Mon, 24 Jun 2013 13:29:16 +0100 Subject: [PATCH] ... --- presentation.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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} -- 2.30.2