pyk.klean.k2lean4 module

class Field(name, ty)[source]

Bases: NamedTuple

name: str: Alias for field number 0

ty: Term: Alias for field number 1

class K2Lean4(defn: 'KoreDefn')[source]

Bases: object

defn: KoreDefn

func_module() → Module[source]

inj_module() → Module[source]

rewrite_module() → Module[source]

sort_module() → Module[source]

property structure_symbols: FrozenDict[str, str]

property structures: FrozenDict[str, tuple[Field, ...]]

property symbol_table: KoreSymbolTable