[Agda] matching to Sum
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Oct 15 13:25:33 CEST 2013
The type hasrepetition A xs is not a datatype unless it can be
reduced (in case xs is a [] or a cons). In your case, it did not
reduce, since the coverage checker did not split on xs due to the
missing [] case.
On 2013-10-15 11:13, Sergei Meshveliani wrote:
> On Tue, 2013-10-15 at 01:07 +0200, Andreas Abel wrote:
>> 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 ())
>
> I see. Thank you
>
> Does the checker report need improvement?
> ("Incomplete pattern matching"
> rather than
> "Cannot split on argument of non-datatype"
> ).
>
> I often advance with implementation by doing the first pattern.
> After I get "Incomplete pattern matching", I see that the given
> patterns
> are checked, and start with the next pattern.
>
> And in this case I was mislead.
> Where is an argument of non-datatype?
>
> Regards,
>
> ------
> Sergei
>
>
>>
>> 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
http://www.tcs.informatik.uni-muenchen.de/~abel/
More information about the Agda
mailing list