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

Internal error when translating a definition #80

Closed asr closed 7 years ago

asr commented 7 years ago 
module Bug where

-- The disjunction data type.
data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

-- A different symbol for disjunction.
_⊕_ : Set → Set → Set
P ⊕ Q = P ∨ Q
{-# ATP definition _⊕_ #-}

postulate
  P Q : Set
  ⊕-comm : P ⊕ Q → Q ⊕ P
{-# ATP prove ⊕-comm #-}
$ apia Bug.agda
An internal error has occurred. Please report this as a bug.
Location of the error: src/Apia/Translation/Functions.hs:188
asr commented 7 years ago

@jechev28 and @jorgeacv2: FYI, when using the ATPs for proving some properties of the exclusive disjunction, I found the above issue.