[Agda] strange mismatch

[Andreas Abel]

Sergei, I think

   {-# OPTIONS --exact-split #-}

will be useful in this case and show you what is going wrong here.

Best,
Andreas

On 24.05.2017 21:35, Sergei Meshveliani wrote:
> On Wed, 2017-05-24 at 22:13 +0300, Sergei Meshveliani wrote:
>> Please, what is wrong here?
>>
>> test1  is type-checked, and  test2  is not
>> (in Agda 2.6.0-207bde6) :
> 
>> -----------------------------------------------------------------------
>> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
>>
>> module _ {α} (A : Set α) (zr a : A)
>>    where
>>    data Expression : Set α where
>>                            con  : A → Expression
>>                            _:+_ : Expression → Expression → Expression
>>
>>    f : Expression → Expression → Expression
>>    f (con zr) y        =  y
>>    f x        (con zr) =  x
>>    f x        y        =  x :+ y
>>
>>    test1 :  f (con zr) (con a) ≡ con a
>>    test1 =  PE.refl
>>
>>    test2 :  f (con a) (con zr) ≡ con a
>>    test2 =  PE.refl
>> ------------------------------------------------------------------------
>>
>> How to fix?
> 
> 
> May be, listing  "zr a"  in parameters does not imply that  a  does not
> match against zr.
> I am not sure.
> 
> May be, I have instead to add to  Expression  the constructors
>      zr : Expression
>      a  : Expression,
> 
> and this will imply that  a  does not match against zr.
> 
> Can anybody comment, please?
> 
> Thanks,
> 
> ------
> Sergei
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/