Странная синтаксическая ошибка

data A = B | C Int

implementation Semigroup A where
  B <+> x = x
  x <+> B = x
  C m <+> C n = C (m + n)

дает мне синтаксическую ошибку

./Nodes/Test.idr:3:1: error: expected: ";",
    "|", declaration, end of input
implementation Semigroup A where 
^                                
Type checking ./Nodes/Test.idr

в Идрисе 0.11.2. Удаление implementation дает вместо этого это сообщение:

./Nodes/Test.idr:3:13: error: expected: "@",
    "with", argument expression,
    constraint argument,
    function right hand side,
    implicit function argument,
    with pattern
Semigroup A where 
            ^     
Type checking ./Nodes/Test.idr

Должен ли я получить сообщение об ошибке? Я не вижу ничего плохого в синтаксисе.

Спасибо.


idris
person RhubarbAndC    schedule 20.06.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы не можете использовать инфиксные операторы в реализациях (на данный момент, я думаю). Вместо этого оберните их префиксами:

data A = B | C Int

implementation Semigroup A where
  (<+>) B x = x
  (<+>) x B = x
  (<+>) (C m) (C n) = C (m + n)
person xash    schedule 20.06.2016
comment
Великолепно! Спасибо. - person RhubarbAndC; 20.06.2016