Skip to content

Commit 4c0264b

Browse files
committed
trying proof annotation
1 parent 56f0734 commit 4c0264b

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

kdrag/kernel.py

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ def __repr__(self):
3030
Proof = None
3131

3232

33-
def is_proof(p):
33+
def is_proof(p: __Proof) -> bool:
3434
return isinstance(p, __Proof)
3535

3636

@@ -45,7 +45,7 @@ def lemma(
4545
timeout=1000,
4646
dump=False,
4747
solver=None,
48-
) -> Proof:
48+
) -> __Proof:
4949
"""Prove a theorem using a list of previously proved lemmas.
5050
5151
In essence `prove(Implies(by, thm))`.
@@ -88,7 +88,7 @@ def lemma(
8888
return __Proof(thm, by, False)
8989

9090

91-
def axiom(thm: smt.BoolRef, by=[]) -> Proof:
91+
def axiom(thm: smt.BoolRef, by=[]) -> __Proof:
9292
"""Assert an axiom.
9393
9494
Axioms are necessary and useful. But you must use great care.

0 commit comments

Comments
 (0)