
<html>


<head>


<meta http-equiv="Content-Type" content="text/html; charset=utf-8">


</head>


<body>


<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">


<div class="PlainText"><br>


<br>


> On 24 Apr 2020, at 18:10, Joey Eremondi <joey.eremondi@gmail.com> wrote:<br>


> <br>


> But our enthusiasm for sized types in Agda was severely dampened when we learned later that in current versions they allow one to prove that true equals false :-( — see <<a href="https://github.com/agda/agda/issues/3026">https://github.com/agda/agda/issues/3026</a>>.<br>


> <br>


> Oh... well that definitely ruins what I was trying to do. Does --sized make Agda inconsistent even with --safe enabled?


<br>


<br>


Yes (see attached, for example).<br>


<br>


Andy<br>


<br>


</div>


</span></font></div>


<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">


<div class="PlainText"><br>


</div>


</span></font></div>


</body>


</html>