Commit 9582e1aa authored by Simon Cruanes's avatar Simon Cruanes
Browse files

tptp2why now recognizes lemma keyword

parent ab80d5f4
......@@ -11,7 +11,7 @@
[
"fof", FOF;
"cnf", CNF;
"lemma", CONJECTURE;
"lemma", LEMMA;
"assumption", AXIOM;
"theorem", CONJECTURE;
"conjecture", CONJECTURE;
......
......@@ -28,7 +28,7 @@
%token<string> UIDENT
%token<string> LIDENT
%token<string> SINGLEQUOTED
%token FOF CNF AXIOM CONJECTURE INCLUDE NEGATED_CONJECTURE
%token FOF CNF AXIOM CONJECTURE INCLUDE NEGATED_CONJECTURE LEMMA
%token EOF
%right PIPE AND ARROW LRARROW
......@@ -57,6 +57,7 @@ decl_type:
| AXIOM { Axiom }
| CONJECTURE { Conjecture }
| NEGATED_CONJECTURE { NegatedConjecture }
| LEMMA { Lemma }
fmla:
......
......@@ -225,6 +225,7 @@ module Translate = struct
| Axiom -> Decl.Paxiom
| Conjecture -> Decl.Pgoal
| NegatedConjecture -> Decl.Pgoal
| Lemma -> Decl.Plemma
(** add a declaration to a theory, after translation *)
let rec addDecl theory = function
......
......@@ -28,6 +28,6 @@ type decl =
| Fof of string * declType * fmla
| Cnf of string * declType * fmla
| Include of string
and declType = Axiom | Conjecture | NegatedConjecture
and declType = Axiom | Conjecture | NegatedConjecture | Lemma
type tptp = decl list
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment