tptp4X found an error

[asr]

From @jechev28 on October 8, 2015 23:52

When testing the file Test.agda the following error is generated:

$ apia --check --atp=vampire --atp=e Test.agda
apia: tptp4X found an error in the file /tmp/Test/24-foo.fof
Please report this as a bug

module Test where

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

infixl 6 _+_
infixl 4 _≡_
infix  8 -_

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

postulate
  +-asso : (x y z : ℝ) → x + y + z ≡ x + (y + z)
  +-neut : (x : ℝ) → x + r₀ ≡ x
  +-inve : (x : ℝ)     → x + (- x) ≡ r₀

{-# ATP axiom +-asso +-neut +-inve #-}

postulate foo : {x y z : ℝ} → x + z ≡ y + z → x ≡ y
{-# ATP prove foo +-inve #-}

[asr]

I added the following test case:

$ cd /test/fail/errors
$ agda DuplicateFormulaTPTP4XError.agda
$ apia --check DuplicateFormulaTPTP4XError.agda
apia: tptp4X found an error/warning in the file /tmp/DuplicateFormulaTPTP4XError/22-foo.fof
Please report this as a bug

ERROR: Duplicate annotated formula name "n12_54442073"

This issue should be handle by EAagda.

[asr]

@jechev28 and @jorgeacv2, is this issue the problem reported in your thesis?

[jechev28]

CC'ing @jorgeacv2. Yes, it is.

[asr]

This is not a bug, but EAgda could generate a warning about the duplication though.