<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Hi Marcus,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
you shouldn't expect to be able to pattern match on functions in regular type theory based on intuitionistic type theory.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
negation is a function so it should be applied to something.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Marcus Christian Lehmann <lehmann@tet.tu-berlin.de><br>
<b>Sent:</b> March 14, 2019 12:36 PM<br>
<b>To:</b> Apostolis Xekoukoulotakis<br>
<b>Cc:</b> agda list<br>
<b>Subject:</b> Re: [Agda] Case split on λ()</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">I have attached a more complete example but it boils down to convincing
<br>
Agda that ¬ 2 ≡ 2 should be empty (following the very readable error <br>
message), e.g.<br>
<br>
```<br>
fun : ¬ (2 ≡ 2) → ⊥<br>
fun () -- Error: "¬ 2 ≡ 2 should be empty, but that's not obvious to me"<br>
```<br>
<br>
<br>
Am 14.03.19 um 09:09 schrieb Apostolis Xekoukoulotakis:<br>
> Marcus, I could not follow your example, but it seems that you are <br>
> trying to case split a function, which is not possible.<br>
><br>
> ```<br>
> open import Relation.Binary.PropositionalEquality<br>
> open import Data.Nat<br>
> open import Data.Empty<br>
> open import Relation.Nullary<br>
><br>
><br>
> fun : ¬ (2 ≡ 2) → ⊥<br>
> fun ¬x = ? -- ⊥-elim (¬x refl)<br>
><br>
> ```<br>
<br>
</div>
</span></font></div>
</body>
</html>