Commands

Commands are top-level functions that operate on the top Theory.

_thy([theory])

Gets theory or the top theory.

Adding extensions

extend(ext[, theory])	Adds extension.
new_base_type(arg1[, theory])	Adds new base type.
new_type_constructor(arg1, arg2[, arg3, theory])	Adds new type constructor.
new_constant(arg1, arg2[, theory])	Adds new (primitive) constant.
new_axiom(arg1[, arg2, theory])	Adds new axiom.
new_definition(arg1, arg2[, theory])	Adds new definition.
new_theorem(arg1[, arg2, theory])	Adds new theorem.
new_python_type_alias(arg1, arg2[, arg3, theory])	Adds new Python type alias.

Removing extensions

reset([arg, theory])

Removes all extensions since arg (inclusive).

Querying extensions

enumerate_extensions(*args[, theory])	Enumerates extensions matching criteria.
lookup_extension(*args[, theory])	Searches for extension.
lookup_type_constructor(*args[, theory])	Searches for type constructor.
lookup_constant(*args[, theory])	Searches for constant.
lookup_axiom(*args[, theory])	Searches for axiom.
lookup_definition(*args[, theory])	Searches for definition.
lookup_theorem(*args[, theory])	Searches for theorem.
lookup_python_type_alias(*args[, theory])	Searches for Python type alias.

Showing extensions

show_extensions(*args[, theory])	Prints extensions matching criteria.
show_type_constructors(*args[, theory])	Prints type constructors matching criteria.
show_constants(*args[, theory])	Prints constants matching criteria.
show_axioms(*args[, theory])	Prints axioms matching criteria.
show_definitions(*args[, theory])	Prints definitions matching criteria.
show_theorems(*args[, theory])	Prints theorems matching criteria.
show_python_type_aliases(*args[, theory])	Prints Python type aliases matching criteria.

Settings

The settings table of the top theory resides in constant settings.

settings

Proxy object.

See Theory.settings.