[Agda] matching to Sum

[Andreas Abel]

The pattern matching is incomplete.  It works with complete pattern 
matching:

cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) = inj₂ (inj₁ y∈xs)
cons-hasRepetition A x (y ∷ xs) (inj₂ h)   = inj₂ (inj₂ h)
cons-hasRepetition A x [] (Level.lift ())


On 12.10.2013 21:38, Sergei Meshveliani wrote:
> Please, why the pattern  (inj₁ y∈xs)   below is checked-out?
>
> I know that
>         cons-hasRepetition A x xs hasRep-xs =  inj₂ hasRep-xs
>
> is sufficient.
> But the question about the pattern  (inj₁ y∈xs)  still remains.
>
>
> -----------------------------------------------------------------
> module Report4 where
> open import Level using (Level; _⊔_; Lift)
> open import Relation.Binary using (Setoid; module Setoid)
> open import Data.Empty    using (⊥)
> open import Data.Sum      using (_⊎_; inj₁; inj₂)
> open import Data.List     using (List; []; _∷_)
> open import Data.List.Any using (module Membership)
>
> --------------------------------------------------------------------
> hasRepetition : ∀ {c l} (A : Setoid c l) → List (Setoid.Carrier A) →
>                                                          Set (c ⊔ l)
> hasRepetition _ []       =  Lift ⊥
> hasRepetition A (x ∷ xs) =  x ∈ xs  ⊎ (hasRepetition A xs)
>                          where
>                          open module MembA = Membership A using (_∈_)
>
> cons-hasRepetition :
>          ∀ {c l} (A : Setoid c l) →
>          let C = Setoid.Carrier A
>          in
>          (x : C) → (xs : List C) → hasRepetition A xs →
>                                    hasRepetition A (x ∷ xs)
>
> cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) =  inj₂ (inj₁ y∈xs)
> --------------------------------------------------------------------
>
> The report is
>
>    Cannot split on argument of non-datatype   hasRepetition A xs
>    when checking the definition of  cons-hasRepetition.


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/