Skip to content

Syntax error in Rocq output due to illegal character in skolem symbols / types #52

@jrosain

Description

@jrosain

Description of the issue

The Rocq output is currently broken in two ways:

  • on output of the context, TPTP's arrow is used instead of Rocq arrow, e.g., Parameter p : goeland_U > Prop instead of Parameter p : goeland_U -> Prop
  • skolem symbols are now written skolem@foo, and the @ is not a valid lexeme for Rocq.

Flags used

-context -orocq

Small problem file to reproduce the bug

% This tests both problems at once
fof(rocq_output_test,conjecture,! [X]: (p(X) | ~p(X))).

Version of Goéland where the issue occurs

This is in the master version (v.1.2-dev.rc9841dae9e19c823410fa0e003a325f8ac1cd44b)

Metadata

Metadata

Assignees

Labels

kind:bugSomething isn't workingpart:rocq-outputAbout the certified output in Rocq

Type

No type

Projects

No projects

Relationships

None yet

Development

No branches or pull requests

Issue actions