[Agda] Case split on λ()

[Marcus Christian Lehmann]

Thank you for pointing this dead-end out.

Therefore I will proceed with

f : ∀ x u v → f x ≡ u → g x ≡ v → u ≡ v ⊎ u ≢ v
f x u v p1 p2 = ?

where proof search seems mighty enough to figure out "inj₁ refl" or 
"inj₂ (λ ())" for the right hand side (after case splitting on x).

regards,

Am 14.03.19 um 17:42 schrieb 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/6620db86/attachment.html>