Multiple arity symbol

[jechev28]

module Bug where

infixr 1 _⊕_

data _⊕_ (A B : Set) : Set where
  inj : A → B → A ⊕ B

postulate
  ℝ : Set

infixl 4 _≡_

data _≡_ : ℝ → ℝ → Set where
  refl : (x : ℝ) → x ≡ x

infixl 4 _>_ _<_

postulate
  _>_ : ℝ → ℝ → Set

_<_ : ℝ → ℝ → Set
y < x = x > y

{-# ATP definition _<_ #-}

postulate
  bar : (x : ℝ) → (x < x) ⊕ (x < x)

{-# ATP axiom bar #-}

postulate foo : (x : ℝ) → x ≡ x
{-# ATP prove foo #-}

$ agda Bug.agda

$ apia --atp=e --check Bug.agda

apia: tptp4X found an error/warning in the file /tmp/Bug/31-foo.fof
Please report this as a bug

WARNING: Line 23 Char 96 Token "," : Multiple arity symbol n_60__24_6263726395305411342, arity 2 and now 0

[asr]

Self question: Duplicated of #96?

CC'ing @jorgeacv2.

[asr]

@jechev28 and @jorgeacv2: I was thinking about this issue.

Let's define xor by

_⊕_ : Set → Set → Set
P ⊕ Q = (P ∨ Q) ∧ ¬ (P ∧ Q)

Can you wrote the above definition in, for example, TPTP? No, you cannot because the above definition is not a FOL-definition.

Let ℝ be our universe of discourse, that, is

postulate
  ℝ : Set

in FOL we can define, n-ary predicates or n-ary functions, that is,

P : ℝ → ... → ℝ → Set  -- n-ary predicate
P = ...

f : ℝ → ... → ℝ   -- n-ary function
f = ...

c : ℝ  -- constant (0-ary function)
c = ...

but we cannot define new logical constants, for example,

_⊕_ : Set → Set → Set
P ⊕ Q = ...

So in the OP (original post), Apia cannot translate the definition of _⊕_ (but it should generates an error though).

[asr]

For a correct error using definitions see #80.