With an empty .apia file, we get an error.

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

With an empty .apia file, we get an error. #66

Open jonaprieto opened 8 years ago

jonaprieto commented 8 years ago

Use an empty file or a file with all lines commented in YAML. An error appears. With:

module NoTheorem where

postulate
  D   : Set
  _≡_ : D → D → Set
  a b : D

postulate foo : a ≡ b
{-# ATP prove foo #-}

Try with an empty .apia:

$ touch .apia
$ apia NoTheorem.agda
apia: UnexpectedEvent {_received = Just EventStreamEnd, _expected = Just EventDocumentStart}

asr commented 8 years ago

@jonaprieto I assigned you this issue.

jonaprieto commented 8 years ago

Ok. I have something in mind to solve this.

asr commented 7 years ago

I'll try to fix this issue.

jonaprieto commented 7 years ago

I was working on this issue in the branch: hotfix/Issue66 but also trying to use parse combinators. I couldn´t resolve the parsing, but it almost complete the integration.

asr commented 7 years ago

I see. Which will be next step?