Function test_match_recursive

tests/test_pattern_match.py:84–121

Nested matching on Name-like types.

(example_lib)

def test_match_recursive(example_lib):
    """Nested matching on Name-like types."""
    # Build a Name.str value manually
    anon = LeanInductiveValue("Name", "anonymous", 0, ())
    name = LeanInductiveValue("Name", "str", 1, (anon, "hello"))

    # Create a simple stand-in for Name type ctors
    class _NameNs:
        pass

    NameNs = _NameNs()
    NameNs.str = _CtorMeta(
        "str",
        (),
        {
            "_ctor_name": "str",
            "_type_name": "Name",
            "_tag": 1,
            "__match_args__": ("_0", "_1"),
        },
    )
    NameNs.anonymous = _CtorMeta(
        "anonymous",
        (),
        {
            "_ctor_name": "anonymous",
            "_type_name": "Name",
            "_tag": 0,
            "__match_args__": (),
        },
    )

    match name:
        case NameNs.str(parent, leaf):
            assert leaf == "hello"
            assert isinstance(parent, NameNs.anonymous)
        case _:
            pytest.fail("Should have matched Name.str")


# ============================================================================