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 #12

Closed asr closed 8 years ago

asr commented 8 years ago

From @asr on March 5, 2013 12:25

{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --universal-quantified-propositional-functions #-}
{-# OPTIONS --without-K #-}

module Bug where

postulate
  D : Set
  ∃ : (A : D → Set) → Set

postulate foo : (A B : D → Set) → ∃ B → ∃ B
{-# ATP prove foo #-}
$ apia Bug.agda
An internal error has occurred. Please report this as a bug.
Location of the error: src/FOL/Translation/Terms.hs:289
asr commented 8 years ago

Fixed.