<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 TRANSITIONAL//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; CHARSET=UTF-8">
<META NAME="GENERATOR" CONTENT="GtkHTML/4.4.4">
</HEAD>
<BODY>
Correction:<BR>
<BR>
I wrote recently about that <BR>
(1) space expence in the Agda-2.4.2.3.20150913 type checker is 3 smaller<BR>
on the DoCon-A library,<BR>
(2) .agdai are smaller.<BR>
<BR>
<BR>
I look now more attentively and see that<BR>
(2) does not hold, the .agdai file sizes are about the same,<BR>
(1) is all right.<BR>
<BR>
------<BR>
Sergei
</BODY>
</HTML>