pyk.klean.k2lean4 module

class BaseMatcher[source]

Bases: Matcher, ABC

var: EVar

class Config[source]

Bases: TypedDict

derive_beq: bool | None

derive_decidableeq: bool | None

class EmptyListMatcher(var: 'EVar')[source]

Bases: BaseMatcher

var: EVar

class EmptyMapMatcher(var: 'EVar', key_sort: 'str', value_sort: 'str')[source]

Bases: BaseMatcher

key_sort: str

value_sort: str

var: EVar

class EmptySetMatcher(var: 'EVar')[source]

Bases: BaseMatcher

var: EVar

class EqMatcher(var1: 'EVar', var2: 'EVar')[source]

Bases: Matcher

var1: EVar

var2: EVar

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', *, config: 'Config | None' = None)[source]

Bases: object

defn: KoreDefn

derive_beq: bool

derive_decidableeq: bool

func_module() → Module[source]

inj_module() → Module[source]

property noncomputable: frozenset[str]

rewrite_module() → Module[source]

sort_module() → Module[source]

property structure_symbols: FrozenDict[str, str]

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

property symbol_table: KoreSymbolTable

class ListMatcher(var: 'EVar', prefix: 'tuple[Pattern, ...]', middle: 'Pattern', suffix: 'tuple[Pattern, ...]')[source]

Bases: BaseMatcher

middle: Pattern

prefix: tuple[Pattern, ...]

suffix: tuple[Pattern, ...]

var: EVar

class MapMatcher(var: 'EVar', key_sort: 'str', value_sort: 'str', keys: 'tuple[Pattern, ...]', values: 'tuple[Pattern, ...]', rest: 'Pattern')[source]

Bases: BaseMatcher

key_sort: str

keys: tuple[Pattern, ...]

rest: Pattern

value_sort: str

values: tuple[Pattern, ...]

var: EVar

class Matcher[source]

Bases: ABC

property inputs: frozenset[EVar]

property outputs: frozenset[EVar]

class SetMatcher(var: 'EVar', elems: 'tuple[Pattern, ...]', rest: 'Pattern')[source]

Bases: BaseMatcher

elems: tuple[Pattern, ...]

rest: Pattern

var: EVar

class SubsortMatcher(var: 'EVar', subsort: 'str', supersort: 'str', pattern: 'Pattern')[source]

Bases: BaseMatcher

pattern: Pattern

subsort: str

supersort: str

var: EVar