Skip to content

Commit

Permalink
Add class Axiom to model
Browse files Browse the repository at this point in the history
  • Loading branch information
tothtamas28 committed Jan 17, 2025
1 parent 57a3bfa commit 86fe32e
Showing 1 changed file with 18 additions and 0 deletions.
18 changes: 18 additions & 0 deletions pyk/src/pyk/k2lean4/model.py
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,24 @@ class Declaration(Command, ABC):
modifiers: Modifiers | None


@final
@dataclass
class Axiom(Declaration):
ident: DeclId
signature: Signature
modifiers: Modifiers | None

def __init__(self, ident: str | DeclId, signature: Signature, modifiers: Modifiers | None = None):
ident = DeclId(ident) if isinstance(ident, str) else ident
object.__setattr__(self, 'ident', ident)
object.__setattr__(self, 'signature', signature)
object.__setattr__(self, 'modifiers', modifiers)

def __str__(self) -> str:
modifiers = f'{self.modifiers} ' if self.modifiers else ''
return f'{modifiers}axiom {self.ident} {self.signature}'


@final
@dataclass
class Abbrev(Declaration):
Expand Down

0 comments on commit 86fe32e

Please sign in to comment.