<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
When you make an mistake on the type of an expression, you may get
the following message<br>
<br>
5 != 4 of type ℕ <br>
when checking that the expression s≤s {n = 4} (s≤s z≤n) <br>
has type 2 ≤ 4<br>
<br>
Why agda doesn't give the type of the expression ? In my example
(coming from an exercise of Philip Wadler)<br>
I would have appreciated the longer message<br>
<br>
5 != 4 of type ℕ<br>
when checking that the expression s≤s {n = 4} (s≤s z≤n) <br>
<b>of type 2 ≤ 5 </b><br>
has type 2 ≤ 4
<div class="moz-signature"><br>
</div>
<div class="moz-signature">-- <br>
mail : <a class="moz-txt-link-abbreviated" href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a> <br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr
</div>
</body>
</html>