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

Method test_lambda_select

tests/test_z3_semantic.py:1321–1325  ·  view source on GitHub ↗

Select(Lambda(x, x + 1), 5) = 6

(self, kernel)

Source from the content-addressed store, hash-verified

1319 """Lambda expression semantics via arrays."""
1320
1321 def test_lambda_select(self, kernel):
1322 """Select(Lambda(x, x + 1), 5) = 6"""
1323 x = Int("x")
1324 f = Lambda([x], x + IntVal(1))
1325 assert _try_prove(Select(f, IntVal(5)) == IntVal(6))
1326
1327 def test_lambda_constant(self, kernel):
1328 """Select(Lambda(x, 42), anything) = 42"""

Callers

nothing calls this directly

Calls 5

IntFunction · 0.90
LambdaFunction · 0.90
IntValFunction · 0.90
_try_proveFunction · 0.90
SelectFunction · 0.90

Tested by

no test coverage detected