Summary
collections.abc types (Iterable, Iterator, Mapping, Sequence, Set, etc.) are stubbed as .none values. While this allows imports to succeed, isinstance() checks against these types always return False.
Current behavior
from collections.abc import Iterable
isinstance([1, 2, 3], Iterable) # Returns False (should be True)
Impact
- Low for current leanSpec E2E coverage — these types are mostly used in type annotations with
from __future__ import annotations (deferred, never evaluated)
- Could affect runtime code that uses
isinstance(x, Iterable) for duck-type dispatch
state/state.py imports Iterable and Set but only uses them in annotations
Possible approach
Implement structural protocol checking: isinstance(x, Iterable) returns True if x has __iter__, etc. This matches CPython's collections.abc behavior via __subclasshook__.
Reference
LeanPython/Interpreter/Eval.lean line 3128-3134 (collections.abc stub)
Summary
collections.abctypes (Iterable,Iterator,Mapping,Sequence,Set, etc.) are stubbed as.nonevalues. While this allows imports to succeed,isinstance()checks against these types always returnFalse.Current behavior
Impact
from __future__ import annotations(deferred, never evaluated)isinstance(x, Iterable)for duck-type dispatchstate/state.pyimportsIterableandSetbut only uses them in annotationsPossible approach
Implement structural protocol checking:
isinstance(x, Iterable)returns True ifxhas__iter__, etc. This matches CPython'scollections.abcbehavior via__subclasshook__.Reference
LeanPython/Interpreter/Eval.leanline 3128-3134 (collections.abc stub)