21 lines
928 B
Python
21 lines
928 B
Python
import unittest
|
|
from lean_agent.core import LeanVerifier, solve, extract
|
|
class Scripted:
|
|
def __init__(self): self.calls = 0
|
|
def complete(self, messages):
|
|
self.calls += 1
|
|
return 'exact False.elim' if self.calls == 1 else 'intro n; rfl'
|
|
class Tests(unittest.TestCase):
|
|
def test_repair(self):
|
|
result = solve(Scripted(), LeanVerifier(), {'id':'x','statement':'∀ n : Nat, n = n'})
|
|
self.assertTrue(result['success'])
|
|
self.assertEqual(len(result['attempts']), 2)
|
|
def test_holes(self):
|
|
for proof in ['sorry', 'admit', 'exact (by sorry)', 'rfl\n#eval 1']:
|
|
self.assertFalse(LeanVerifier().check('1 = 1', proof).success)
|
|
def test_false(self):
|
|
self.assertFalse(LeanVerifier().check('False', 'trivial').success)
|
|
def test_extract(self):
|
|
self.assertEqual(extract('```lean\nby\n rfl\n```'), 'rfl')
|
|
if __name__ == '__main__': unittest.main()
|