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

Attributes

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