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
object list
object listdrop
object listfold
object listlength
object logic
object nat
object natdivisible
object natdivision
object natlists
object natorder
object props
object set
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