<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Thank you for pointing this dead-end
out.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Therefore I will proceed with<br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">f : ∀ x u v → f x ≡ u → g x ≡ v → u ≡ v
⊎ u ≢ v</div>
<div class="moz-cite-prefix">f x u v p1 p2 = ?</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">where proof search seems mighty enough
to figure out "inj₁ refl" or "inj₂ (λ ())" for the right hand side
(after case splitting on x).</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">regards,</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Am 14.03.19 um 17:42 schrieb Jason
-Zhong Sheng- Hu:<br>
</div>
<blockquote type="cite"
cite="mid:YTXPR0101MB14729E0CEACD1DEEBB9652EEAF4B0@YTXPR0101MB1472.CANPRD01.PROD.OUTLOOK.COM">
<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</b></span></span></font> </div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt"
face="Calibri, sans-serif" color="#000000"><b>From:</b> Agda
<a class="moz-txt-link-rfc2396E" href="mailto:agda-bounces@lists.chalmers.se"><agda-bounces@lists.chalmers.se></a> on behalf of Marcus
Christian Lehmann <a class="moz-txt-link-rfc2396E" href="mailto:lehmann@tet.tu-berlin.de"><lehmann@tet.tu-berlin.de></a><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>
</blockquote>
<br>
</body>
</html>