[Agda] inversion

[Jesper Cockx]

Yep, Agda has such a feature: it's called dependent pattern matching.

inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n
inversionEven (evenSS x) = x

-- Jesper

On Tue, Feb 19, 2019 at 6:17 PM Pierre Lescanne (en) <
pierre.lescanne at ens-lyon.fr> wrote:

> Assuming a predicate *even*
>
> *data even :  ℕ -> Set where*
> *  even0 : even zero*
> *  even1 : even (suc zero)*
> *  evenSS : {n : ℕ} -> even n -> even (suc (suc n))*
>
> I would like to prove:
>
> *inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n*
>
> In Coq, I could use
>
>    - either a command *inversion*
>    - or a somewhat direct proof that applies even_ind.
>
> Are there similar features in Agda ?
>
> --
> Cheers
>
> ---------------------------
> Pierre Lescanne (Emeritus Professor)
> LIP / École normale supérieure de Lyon
> 46 allée d'Italie
> 69364 LYON Cedex 07, France
> tél: +33 6 85 70 94 31http://perso.ens-lyon.fr/pierre.lescanne/
> ---------------------------
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190219/df0fca1e/attachment.html>