[Agda] a puzzle about pattern matching

[Matteo Acerbi]

I agree, in this case it is simpler.

Sometimes equality is not decidable, though.

Even when it is, if the cases are more than two I would avoid nested checks...

Cheers,
Matteo

On Tue, Apr 14, 2015 at 12:32 AM, effectfully <effectfully at gmail.com> wrote:
> Matteo Acerbi, in this case it's easier to just use decidable equality:
>
> open import Relation.Nullary
> open import Relation.Binary
>
> postulate
>   _≟A_ : Decidable (_≡_ {A = A})
>
> action : A → A
> action x with x ≟A d a a a
> ... | yes _  = d a a a
> ... | no  _  = a
>
> lem : ∀(x : A) → x ≢ d a a a → action x ≡ a
> lem x c with x ≟A d a a a
> ... | yes p = ⊥-elim (c p)
> ... | no  _ = refl