[Agda] a puzzle about pattern matching

[Aaron Stump]

Dear Jacques, Matteo, and effectfully,

Thanks a lot for these answers.  They are all enlightening for me. I 
think was looking particularly for the view method.  This is really helpful.

Best wishes,
Aaron

On 04/13/2015 05:47 PM, Matteo Acerbi wrote:
> 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