MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / test_frontend_process_simple

Function test_frontend_process_simple

tests/test_kernel_extra.py:48–52  ·  view source on GitHub ↗
(kernel)

Source from the content-addressed store, hash-verified

46
47
48def test_frontend_process_simple(kernel):
49 src = "def foo : Nat := 42\n"
50 out = kernel.process(src)
51 # New constants from the def should be present.
52 assert "foo" in out
53
54
55def test_frontend_collect_sorrys_no_sorries(kernel):

Callers

nothing calls this directly

Calls 1

processMethod · 0.80

Tested by

no test coverage detected