gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.formats/gapt.formats.leancop/LeanCoP21Parser

LeanCoP21Parser

gapt.formats.leancop.LeanCoP21Parser
object LeanCoP21Parser

Attributes

Source
LeanCoP21Parser.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Type members

Classlikes

case class Clause(literals: Lit*)

Attributes

Source
LeanCoP21Parser.scala
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
case object Hash extends Lit

Attributes

Source
LeanCoP21Parser.scala
Supertypes
trait Singleton
trait Product
trait Mirror
trait Serializable
trait Product
trait Equals
trait Lit
class Object
trait Matchable
class Any
Show all
Self type
Hash.type
sealed trait Lit

Attributes

Source
LeanCoP21Parser.scala
Supertypes
class Object
trait Matchable
class Any
Known subtypes
object Hash.type
class Neg
object NegHash.type
class Pos
case class Neg(atom: FOLAtom) extends Lit

Attributes

Source
LeanCoP21Parser.scala
Supertypes
trait Serializable
trait Product
trait Equals
trait Lit
class Object
trait Matchable
class Any
Show all
case object NegHash extends Lit

Attributes

Source
LeanCoP21Parser.scala
Supertypes
trait Singleton
trait Product
trait Mirror
trait Serializable
trait Product
trait Equals
trait Lit
class Object
trait Matchable
class Any
Show all
Self type
NegHash.type
case class Pos(atom: FOLAtom) extends Lit

Attributes

Source
LeanCoP21Parser.scala
Supertypes
trait Serializable
trait Product
trait Equals
trait Lit
class Object
trait Matchable
class Any
Show all
case class Proof(main: Clause, sides: List[Proof])

Attributes

Source
LeanCoP21Parser.scala
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all

Value members

Concrete methods

def atom[X : ParsingRun]: ParsingRun[FOLAtom]

Attributes

Source
LeanCoP21Parser.scala
def clause[X : ParsingRun]: ParsingRun[Clause]

Attributes

Source
LeanCoP21Parser.scala
def hash[X : ParsingRun]: ParsingRun[Lit]

Attributes

Source
LeanCoP21Parser.scala
def ident[X : ParsingRun]: ParsingRun[String]

Attributes

Source
LeanCoP21Parser.scala
def lit[X : ParsingRun]: ParsingRun[Lit]

Attributes

Source
LeanCoP21Parser.scala
def neg[X : ParsingRun]: ParsingRun[Lit]

Attributes

Source
LeanCoP21Parser.scala
def negHash[X : ParsingRun]: ParsingRun[Lit]

Attributes

Source
LeanCoP21Parser.scala
def parse(stdout: String): Either[String, Proof]

Attributes

Source
LeanCoP21Parser.scala
def pos[X : ParsingRun]: ParsingRun[Lit]

Attributes

Source
LeanCoP21Parser.scala
def proof[X : ParsingRun]: ParsingRun[Proof]

Attributes

Source
LeanCoP21Parser.scala
def stdout[X : ParsingRun]: ParsingRun[Proof]

Attributes

Source
LeanCoP21Parser.scala
def term[X : ParsingRun]: ParsingRun[FOLTerm]

Attributes

Source
LeanCoP21Parser.scala
Generated with