git @ Cat's Eye Technologies Eqthy / master src / eqthy / objects.py
master

Tree @master (Download .tar.gz)

objects.py @master — raw · history · blame 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
# Copyright (c) 2022-2024 Chris Pressey, Cat's Eye Technologies
# This file is distributed under a 2-clause BSD license.  See LICENSES directory:
# SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Eqthy

"""Objects in the Eqthy document structure."""
from dataclasses import dataclass
from typing import List, Union
from .terms import Eqn, Term, Variable


class Hint:
    pass


@dataclass(frozen=True)
class Reflexivity(Hint):
    pass


@dataclass(frozen=True)
class Substitution(Hint):
    term: Term
    variable: Variable


@dataclass(frozen=True)
class Congruence(Hint):
    term: Term
    variable: Variable


@dataclass(frozen=True)
class Reference(Hint):
    name: str
    side: Union[str, None]
    substs: List[Eqn]


# proof objects

@dataclass(frozen=True)
class Axiom:
    name: str
    eqn: Eqn


@dataclass(frozen=True)
class Step:
    eqn: Eqn
    hint: Union[Hint, None]


@dataclass(frozen=True)
class Theorem:
    name: str
    eqn: Eqn
    steps: List[Step]


@dataclass(frozen=True)
class Document:
    axioms: List[Axiom]
    theorems: List[Theorem]