pyk.k2lean4.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 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'
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 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
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 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(commands: 'Iterable[Command] | None' = None)[source]

Bases: object

commands: tuple[Command, ...]
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 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]