search

asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic
MIT License
6 stars 0 forks source link

Error when translating schematic-propositional-symbols and not hard-coded symbols #96

Open asr opened 7 years ago

asr commented 7 years ago 
postulate
  _⋆_ : Set → Set → Set
  foo : {P Q : Set} → P ⋆ Q → Q ⋆ P

{-# ATP prove foo #-}
$ agda Bug.agda
$ apia --atp=e --check --schematic-propositional-symbols Bug.agda
apia: tptp4X found an error/warning in the file /tmp/Bug/4-foo.fof
Please report this as a bug

ERROR: Line 12 Char 78 Token "," continuing with "B) => kp2_(n_8902__"

The error disappears if I replace _⋆_ by the hard-coded _∨_.