[Agda] Case split on λ()

[Jason -Zhong Sheng- Hu]

Hi Marcus,

you shouldn't expect to be able to pattern match on functions in regular type theory based on intuitionistic type theory.

negation is a function so it should be applied to something.

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Marcus Christian Lehmann <lehmann at tet.tu-berlin.de>
Sent: March 14, 2019 12:36 PM
To: Apostolis Xekoukoulotakis
Cc: agda list
Subject: Re: [Agda] Case split on λ()

I have attached a more complete example but it boils down to convincing
Agda that ¬ 2 ≡ 2 should be empty (following the very readable error
message), e.g.

```
fun : ¬ (2 ≡ 2) → ⊥
fun () -- Error: "¬ 2 ≡ 2 should be empty, but that's not obvious to me"
```


Am 14.03.19 um 09:09 schrieb Apostolis Xekoukoulotakis:
> Marcus, I could not follow your example, but it seems that you are
> trying to case split a function, which is not possible.
>
> ```
> open import Relation.Binary.PropositionalEquality
> open import Data.Nat
> open import Data.Empty
> open import Relation.Nullary
>
>
> fun : ¬ (2 ≡ 2) → ⊥
> fun ¬x =  ? -- ⊥-elim (¬x refl)
>
> ```

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190314/47acd0ac/attachment.html>