Theory

gapt.examples.theories.Theory
See theTheory companion object
class Theory(imports: Theory*) extends Theory0

Models a mathematical theory, i.e. definitions of data types, sorts, constants, etc. (contained in a gapt.proofs.context.Context), together with proofs about these objects.

Value parameters

imports

A list of theories that this theory is based upon.

Attributes

Companion
object
Graph
Supertypes
class Theory0
class Object
trait Matchable
class Any
Known subtypes
object fta.type
object list.type
object listdrop.type
object listfold.type
object listlength.type
object logic.type
object nat.type
object natdivisible.type
object natdivision.type
object natlists.type
object natorder.type
object props.type
object set.type
Show all

Members list

Type members

Classlikes

case class LemmaHandle(proofName: Expr)

Captures an LKProof together with the set of previous lemmas used in it.

Captures an LKProof together with the set of previous lemmas used in it.

Attributes

Companion
object
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
object LemmaHandle

Attributes

Companion
class
Supertypes
trait Product
trait Mirror
class Object
trait Matchable
class Any
Self type

Value members

Concrete methods

def ctxWithProofDefinitions(): ImmutableContext
def main(args: Array[String]): Unit
def proof(name: String): LKProof

Inherited methods

Attributes

Inherited from:
Theory0

Concrete fields

Implicits

Inherited implicits

implicit def ctx: Context

Attributes

Inherited from:
Theory0