Different functions (same name, different arity) are translate using the same name

[asr]

From @jechev28 on October 3, 2015 16:54

We wanted to prove the theorem --neut using the ATP E 1.9 and the following error was generated:

$ agda Bug.agda 
Skipping Bug (/tmp/Bug.agdai).
$ apia --atp=e Bug.agda
Proving the conjecture in /tmp/Bug/20-9472-neut.fof
eprover: /tmp/Bug/20-9472-neut.fof:12:(Column 54):n45 used with arity 1, but registered with arity 2
E 1.9 Sourenee *did not* prove the conjecture
apia: the ATP(s) did not prove the conjecture in /tmp/Bug/20-9472-neut.fof

Tested with Agda 2.4.3.1.

module  Bug where

postulate
  ℝ   : Set
  r₀  : ℝ
  _+_ : ℝ → ℝ → ℝ
  -_  : ℝ → ℝ

_-_ : ℝ → ℝ → ℝ
x - y = x + (- y)

infixl 4 _≡_

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

postulate ─-neut : {x : ℝ} → r₀ - x ≡ - x
{-# ATP prove ─-neut #-}

[asr]

Tested with Agda 2.4.3.1.

Since Apia only compiles with Agda 2.4.3.1 the above information isn't needed.

[asr]

Fixed by 9f1eccb.