pyk.k2lean4 package

Submodules

• pyk.k2lean4.k2lean4 module
  • K2Lean4
    • K2Lean4.defn
    • K2Lean4.sort_module()
• pyk.k2lean4.model module
  • Abbrev
    • Abbrev.ident
    • Abbrev.modifiers
    • Abbrev.signature
    • Abbrev.val
  • Attr
    • Attr.attr
    • Attr.kind
  • AttrKind
    • AttrKind.LOCAL
    • AttrKind.SCOPED
  • Binder
  • BracketBinder
  • Command
  • Ctor
    • Ctor.ident
    • Ctor.modifiers
    • Ctor.signature
  • DeclId
    • DeclId.uvars
    • DeclId.val
  • Declaration
    • Declaration.modifiers
  • ExplBinder
    • ExplBinder.idents
    • ExplBinder.ty
  • ImplBinder
    • ImplBinder.idents
    • ImplBinder.strict
    • ImplBinder.ty
  • Inductive
    • Inductive.ctors
    • Inductive.deriving
    • Inductive.ident
    • Inductive.modifiers
    • Inductive.signature
  • InstBinder
    • InstBinder.ident
    • InstBinder.ty
  • Modifiers
    • Modifiers.attrs
    • Modifiers.noncomputable
    • Modifiers.totality
    • Modifiers.unsafe
    • Modifiers.visibility
  • Module
    • Module.commands
  • Mutual
    • Mutual.commands
  • Signature
    • Signature.binders
    • Signature.ty
  • Term
    • Term.term
  • Totality
    • Totality.NONREC
    • Totality.PARTIAL
  • Visibility
    • Visibility.PRIVATE
    • Visibility.PROTECTED
  • indent()