gapt.examples.theories

Members list

Type members

Classlikes

object Theory

Attributes

Companion
class
Supertypes
class Object
trait Matchable
class Any
Self type
Theory.type
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.

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
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
class Theory0(val imports: List[Theory])

Attributes

Supertypes
class Object
trait Matchable
class Any
Known subtypes
class Theory
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
object fta extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
fta.type
object list extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
list.type
object listdrop extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
listdrop.type
object listfold extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
listfold.type
object listlength extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
listlength.type
object logic extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
logic.type
object nat extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
nat.type
object natdivisible extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
object natdivision extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
object natlists extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
natlists.type
object natorder extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
natorder.type
object props extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
props.type
object set extends Theory

Attributes

Supertypes
class Theory
class Theory0
class Object
trait Matchable
class Any
Self type
set.type