Skip to main content

Ctrl+K

ulkb documentation

Site Navigation

Object
Expression
Type constructor
Type
Term

Conversion, parsing, serialization

Appendix: More object methods

Appendix: Utilities

Site Navigation

Object
Expression
Type constructor
Type
Term

Conversion, parsing, serialization

Appendix: More object methods

Appendix: Utilities

Section Navigation

ulkb.Theory.top
ulkb.Theory.push
ulkb.Theory.pop

ulkb.Theory.extend
ulkb.Theory.new_base_type
ulkb.Theory.new_type_constructor
ulkb.Theory.new_constant
ulkb.Theory.new_axiom
ulkb.Theory.new_definition
ulkb.Theory.new_theorem
ulkb.Theory.new_python_type_alias

ulkb.Theory.reset

ulkb.Theory.enumerate_extensions
ulkb.Theory.lookup_extension
ulkb.Theory.lookup_type_constructor
ulkb.Theory.lookup_constant
ulkb.Theory.lookup_axiom
ulkb.Theory.lookup_definition
ulkb.Theory.lookup_theorem
ulkb.Theory.lookup_python_type_alias

ulkb.Theory.show_extensions

ulkb.Theory.load

ulkb.Theory.prelude
ulkb.Theory.get_prelude
ulkb.Theory.prelude_offset
ulkb.Theory.get_prelude_offset
ulkb.Theory.args_no_prelude
ulkb.Theory.get_args_no_prelude

ulkb.Theory.settings
ulkb.Theory.get_settings

ulkb.TheorySettings.graph
ulkb.TheorySettings.converter
ulkb.TheorySettings.parser
ulkb.TheorySettings.serializer
ulkb.TheorySettings.generated_id_prefix
ulkb.TheorySettings.record_proofs
ulkb.TheorySettings.override_object_repr
ulkb.TheorySettings.debug

Theory
ulkb.Theory.args_no_prelude

ulkb.Theory.args_no_prelude#

property Theory.args_no_prelude#: Theory arguments excluding prelude extensions.

previous

ulkb.Theory.get_prelude_offset

next

ulkb.Theory.get_args_no_prelude

On this page

Theory.args_no_prelude

© Copyright 2023, IBM Corp.

Created using Sphinx 7.2.2.

Built with the PyData Sphinx Theme 0.13.3.