gapt-examples
API
Generated with
gapt-examples/gapt.examples/gapt.examples.theories/listlength

listlength

gapt.examples.theories.listlength
object listlength extends Theory

Attributes

Graph
Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
listlength.type

Members list

Type members

Inherited 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

Inherited from:
Theory
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
object LemmaHandle

Attributes

Inherited from:
Theory
Supertypes
trait Product
trait Mirror
class Object
trait Matchable
class Any

Value members

Inherited methods

def allProofs: Vector[(String, Eval[DelayedProofResult])]

Attributes

Inherited from:
Theory
def ctxWithProofDefinitions(): ImmutableContext

Attributes

Inherited from:
Theory
def main(args: Array[String]): Unit

Attributes

Inherited from:
Theory
def proof(name: String): LKProof

Attributes

Inherited from:
Theory
def proofsHere: Vector[(String, Eval[DelayedProofResult])]

Attributes

Inherited from:
Theory0

Concrete fields

Inherited fields

val imports: List[Theory]

Attributes

Inherited from:
Theory0
val transitiveImports: Vector[Theory]

Attributes

Inherited from:
Theory

Implicits

Inherited implicits

implicit def ctx: Context

Attributes

Inherited from:
Theory0
Generated with