pyk.klean package

Submodules

• pyk.klean.generate module
  • GenContext
    • GenContext.library_name
    • GenContext.package_name
  • generate()
• pyk.klean.k2lean4 module
  • BaseMatcher
    • BaseMatcher.var
  • Config
    • Config.derive_beq
    • Config.derive_decidableeq
  • EmptyListMatcher
    • EmptyListMatcher.var
  • EmptyMapMatcher
    • EmptyMapMatcher.key_sort
    • EmptyMapMatcher.value_sort
    • EmptyMapMatcher.var
  • EmptySetMatcher
    • EmptySetMatcher.var
  • EqMatcher
    • EqMatcher.var1
    • EqMatcher.var2
  • Field
    • Field.name
    • Field.ty
  • K2Lean4
    • K2Lean4.defn
    • K2Lean4.derive_beq
    • K2Lean4.derive_decidableeq
    • K2Lean4.func_module()
    • K2Lean4.inj_module()
    • K2Lean4.noncomputable
    • K2Lean4.rewrite_module()
    • K2Lean4.sort_module()
    • K2Lean4.structure_symbols
    • K2Lean4.structures
    • K2Lean4.symbol_table
  • ListMatcher
    • ListMatcher.middle
    • ListMatcher.prefix
    • ListMatcher.suffix
    • ListMatcher.var
  • MapMatcher
    • MapMatcher.key_sort
    • MapMatcher.keys
    • MapMatcher.rest
    • MapMatcher.value_sort
    • MapMatcher.values
    • MapMatcher.var
  • Matcher
    • Matcher.inputs
    • Matcher.outputs
  • SetMatcher
    • SetMatcher.elems
    • SetMatcher.rest
    • SetMatcher.var
  • SubsortMatcher
    • SubsortMatcher.pattern
    • SubsortMatcher.subsort
    • SubsortMatcher.supersort
    • SubsortMatcher.var
• pyk.klean.model module
  • Abbrev
    • Abbrev.ident
    • Abbrev.modifiers
    • Abbrev.signature
    • Abbrev.val
  • Alt
    • Alt.patterns
    • Alt.rhs
  • AltsFieldVal
    • AltsFieldVal.alts
  • AltsVal
    • AltsVal.alts
  • Attr
    • Attr.attr
    • Attr.kind
  • AttrKind
    • AttrKind.LOCAL
    • AttrKind.SCOPED
  • Axiom
    • Axiom.ident
    • Axiom.modifiers
    • Axiom.signature
  • Binder
  • BracketBinder
  • Command
  • Ctor
    • Ctor.ident
    • Ctor.modifiers
    • Ctor.signature
  • DeclId
    • DeclId.uvars
    • DeclId.val
  • DeclVal
  • Declaration
    • Declaration.modifiers
  • Definition
    • Definition.deriving
    • Definition.ident
    • Definition.modifiers
    • Definition.signature
    • Definition.val
  • ExplBinder
    • ExplBinder.idents
    • ExplBinder.ty
  • FieldVal
  • ImplBinder
    • ImplBinder.idents
    • ImplBinder.strict
    • ImplBinder.ty
  • Inductive
    • Inductive.ctors
    • Inductive.deriving
    • Inductive.ident
    • Inductive.modifiers
    • Inductive.signature
  • InstBinder
    • InstBinder.ident
    • InstBinder.ty
  • InstField
    • InstField.lval
    • InstField.signature
    • InstField.val
  • Instance
    • Instance.attr_kind
    • Instance.ident
    • Instance.modifiers
    • Instance.priority
    • Instance.signature
    • Instance.val
  • Modifiers
    • Modifiers.attrs
    • Modifiers.noncomputable
    • Modifiers.totality
    • Modifiers.unsafe
    • Modifiers.visibility
  • Module
    • Module.commands
    • Module.imports
  • Mutual
    • Mutual.commands
  • Signature
    • Signature.binders
    • Signature.ty
  • SimpleFieldVal
    • SimpleFieldVal.term
  • SimpleVal
    • SimpleVal.term
  • StructCtor
    • StructCtor.fields
    • StructCtor.ident
  • StructIdent
    • StructIdent.ident
    • StructIdent.modifiers
  • StructVal
    • StructVal.fields
  • Structure
    • Structure.ctor
    • Structure.deriving
    • Structure.extends
    • Structure.ident
    • Structure.modifiers
    • Structure.signature
  • Term
    • Term.term
  • Totality
    • Totality.NONREC
    • Totality.PARTIAL
  • Visibility
    • Visibility.PRIVATE
    • Visibility.PROTECTED
  • indent()