Skip to main content
Ctrl+K

ulkb documentation

Site Navigation

  • Object
  • Expression
  • Type constructor
  • Type
  • Term
  • Prelude
  • Extension
  • Theory
  • Commands
  • Conversion, parsing, serialization
  • Appendix: More object methods
  • Appendix: Utilities

Site Navigation

  • Object
  • Expression
  • Type constructor
  • Type
  • Term
  • Prelude
  • Extension
  • Theory
  • Commands
  • Conversion, parsing, serialization
  • Appendix: More object methods
  • Appendix: Utilities

Section Navigation

  • ulkb._thy
  • ulkb.extend
  • ulkb.new_base_type
  • ulkb.new_type_constructor
  • ulkb.new_constant
  • ulkb.new_axiom
  • ulkb.new_definition
  • ulkb.new_theorem
  • ulkb.new_python_type_alias
  • ulkb.reset
  • ulkb.enumerate_extensions
  • ulkb.lookup_extension
  • ulkb.lookup_type_constructor
  • ulkb.lookup_constant
  • ulkb.lookup_axiom
  • ulkb.lookup_definition
  • ulkb.lookup_theorem
  • ulkb.lookup_python_type_alias
  • ulkb.show_extensions
  • ulkb.show_type_constructors
  • ulkb.show_constants
  • ulkb.show_axioms
  • ulkb.show_definitions
  • ulkb.show_theorems
  • ulkb.show_python_type_aliases
  • ulkb.settings
  • Commands
  • ulkb.new_definition

ulkb.new_definition#

new_definition(arg1, arg2, theory=None, **kwargs)[source]#

Adds new definition.

See Theory.new_definition().

previous

ulkb.new_axiom

next

ulkb.new_theorem
On this page
  • new_definition()
Show Source

© Copyright 2023, IBM Corp.

Created using Sphinx 7.2.2.

Built with the PyData Sphinx Theme 0.13.3.