Theory

class Theory(*args, load_prelude=True, **kwargs)

Bases: Object

The state of the logic developments so far.

A Theory consists of a sequence of extensions (Extension).

Multiple Theory objects can coexist, but at any time only one of them is the current or top theory. By default, commands and other top-level functions operate over the top theory.

The top theory can be accessed using Theory.top or _thy(). It can be changed using Theory.push() and restored using Theory.pop().

Parameters:

• args – Extensions.

• load_prelude – Whether to load the standard prelude.

• kwargs – Annotations.

Returns:

Theory.

Theory stack

Theory.top	The top theory.
Theory.push(theory)	Pushes theory onto theory stack.
Theory.pop()	Pops theory from theory stack.

Adding extensions

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

Removing extensions

Theory.reset([arg])

Removes all extensions since arg (inclusive).

Querying extensions

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

Showing extensions

Theory.show_extensions(*args[, limit, ...])

Prints extensions matching criteria.

Modules

Theory.load(mod_name)

Loads module into theory.

Prelude

Theory.prelude	Prelude module or None (not loaded).
Theory.get_prelude()	Gets prelude module.
Theory.prelude_offset	Start index of non-prelude extensions.
Theory.get_prelude_offset()	Gets start index of non-prelude extensions.
Theory.args_no_prelude	Theory arguments excluding prelude extensions.
Theory.get_args_no_prelude()	Gets theory arguments excluding prelude extensions.

Settings

Theory.settings	Theory settings table.
Theory.get_settings()	Gets theory settings table.

The theory settings table is an instance of TheorySettings.

class TheorySettings(**kwargs)

Theory settings.

TheorySettings.graph	alias of GraphSettings
TheorySettings.converter	alias of ConverterSettings
TheorySettings.parser	alias of ParserSettings
TheorySettings.serializer	alias of SerializerSettings
TheorySettings.generated_id_prefix	Prefix of generated ids.
TheorySettings.record_proofs	Whether to record proofs.
TheorySettings.override_object_repr	Whether to override Object.__repr__().
TheorySettings.debug	Whether to enable debugging.