pyk.klean.model module

final class Abbrev(ident: 'str | DeclId', val: 'Term', signature: 'Signature | None' = None, modifiers: 'Modifiers | None' = None)[source]

Bases: Declaration

ident: DeclId
modifiers: Modifiers | None
signature: Signature | None
val: Term
final class Alt(patterns: 'Iterable[Term]', rhs: 'Term')[source]

Bases: object

patterns: tuple[Term, ...]
rhs: Term
final class AltsFieldVal(alts: 'Iterable[Alt]')[source]

Bases: FieldVal

alts: tuple[Alt, ...]
final class Attr(attr: 'str', kind: 'AttrKind | None' = None)[source]

Bases: object

attr: str
kind: AttrKind | None
class AttrKind(value)[source]

Bases: Enum

An enumeration.

LOCAL = 'local'
SCOPED = 'scoped'
final class Axiom(ident: 'str | DeclId', signature: 'Signature', modifiers: 'Modifiers | None' = None)[source]

Bases: Declaration

ident: DeclId
modifiers: Modifiers | None
signature: Signature
class Binder[source]

Bases: ABC

class BracketBinder[source]

Bases: Binder, ABC

class Command[source]

Bases: ABC

final class Ctor(ident: 'str', signature: 'Signature | None' = None, modifiers: 'Modifiers | None' = None)[source]

Bases: object

ident: str
modifiers: Modifiers | None = None
signature: Signature | None = None
final class DeclId(val: 'str', uvars: 'Iterable[str] | None' = None)[source]

Bases: object

uvars: tuple[str, ...]
val: str
class DeclVal[source]

Bases: ABC

class Declaration[source]

Bases: Command, ABC

modifiers: Modifiers | None
final class ExplBinder(idents: 'Iterable[str]', ty: 'Term | None' = None)[source]

Bases: BracketBinder

idents: tuple[str, ...]
ty: Term | None
class FieldVal[source]

Bases: ABC

final class ImplBinder(idents: 'Iterable[str]', ty: 'Term | None' = None, *, strict: 'bool | None' = None)[source]

Bases: BracketBinder

idents: tuple[str, ...]
strict: bool
ty: Term | None
final class Inductive(ident: 'str | DeclId', signature: 'Signature | None' = None, ctors: 'Iterable[Ctor] | None' = None, deriving: 'Iterable[str] | None' = None, modifiers: 'Modifiers | None' = None)[source]

Bases: Declaration

ctors: tuple[Ctor, ...]
deriving: tuple[str, ...]
ident: DeclId
modifiers: Modifiers | None
signature: Signature | None
final class InstBinder(ty: 'Term', ident: 'str | None' = None)[source]

Bases: BracketBinder

ident: str | None
ty: Term
final class InstField(lval: 'str', val: 'FieldVal', signature: 'Signature | None' = None)[source]

Bases: object

lval: str
signature: Signature | None
val: FieldVal
final class Instance(signature: 'Signature', val: 'DeclVal', attr_kind: 'AttrKind | None' = None, priority: 'int | None' = None, ident: 'str | DeclId | None' = None, modifiers: 'Modifiers | None' = None)[source]

Bases: Declaration

attr_kind: AttrKind | None
ident: DeclId | None
modifiers: Modifiers | None
priority: int | None
signature: Signature
val: DeclVal
final class Modifiers(*, attrs: 'Iterable[str | Attr] | None' = None, visibility: 'str | Visibility | None' = None, noncomputable: 'bool | None' = None, unsafe: 'bool | None' = None, totality: 'str | Totality | None' = None)[source]

Bases: object

attrs: tuple[Attr, ...]
noncomputable: bool
totality: Totality | None
unsafe: bool
visibility: Visibility | None
final class Module(imports: 'Iterable[str] | None' = None, commands: 'Iterable[Command] | None' = None)[source]

Bases: object

commands: tuple[Command, ...]
imports: tuple[str, ...]
class Mutual(commands: Iterable[Command] | None = None)[source]

Bases: Command

commands: tuple[Command, ...]
final class Signature(binders: 'Iterable[Binder] | None' = None, ty: 'Term | None' = None)[source]

Bases: object

binders: tuple[Binder, ...]
ty: Term | None
final class SimpleFieldVal(term: 'Term')[source]

Bases: FieldVal

term: Term
final class SimpleVal(term: 'Term')[source]

Bases: DeclVal

term: Term
final class StructCtor(fields: 'Iterable[Binder]', ident: 'str | StructIdent | None' = None)[source]

Bases: object

fields: tuple[Binder, ...]
ident: StructIdent | None
final class StructIdent(ident: 'str', modifiers: 'Modifiers | None' = None)[source]

Bases: object

ident: str
modifiers: Modifiers | None = None
final class StructVal(fields: 'Iterable[InstField]')[source]

Bases: DeclVal

fields: tuple[InstField, ...]
final class Structure(ident: 'str | DeclId', signature: 'Signature | None' = None, extends: 'Iterable[Term] | None' = None, ctor: 'StructCtor | None' = None, deriving: 'Iterable[str] | None' = None, modifiers: 'Modifiers | None' = None)[source]

Bases: Declaration

ctor: StructCtor | None
deriving: tuple[str, ...]
extends: tuple[Term, ...]
ident: DeclId
modifiers: Modifiers | None
signature: Signature | None
final class Term(term: 'str')[source]

Bases: object

term: str
class Totality(value)[source]

Bases: Enum

An enumeration.

NONREC = 'nonrec'
PARTIAL = 'partial'
class Visibility(value)[source]

Bases: Enum

An enumeration.

PRIVATE = 'private'
PROTECTED = 'protected'
indent(text: str, n: int) → str[source]