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

All the arguments are required in an ATP definition #11

Open asr opened 8 years ago

asr commented 8 years ago

From @asr on February 24, 2013 22:7

postulate
  D          : Set
  false true : D

data Bool : D → Set where
  btrue  : Bool true
  bfalse : Bool false

OkBit : D → Set
OkBit b = Bool b
{-# ATP definition OkBit #-}

postulate foo : ∀ b → OkBit b → OkBit b
{-# ATP prove foo #-}

WrongBit : D → Set
WrongBit = Bool
{-# ATP definition WrongBit #-}

postulate bar : ∀ b → WrongBit b → WrongBit b
{-# ATP prove bar #-}

-- $ apia --check Bug.agda
-- apia: tptp4X found an error/warning in the file /tmp/Bug/20-bar.fof
-- Please report this as a bug
--
-- ERROR: Line 12 Char 83 Token ")" continuing with ")).
-- "
asr commented 8 years ago

The fix requires the fix of the Agda issue https://github.com/agda/agda/issues/775.