python-to-lean4-translator
Installation
SKILL.md
Python → Lean 4 Translator
This is a delta over → c-cpp-to-lean4-translator — same target, easier memory model (no pointers), harder type discipline (dynamic → dependent).
Python-specific mappings
| Python | Lean |
|---|---|
int |
Int — both unbounded. The easy case. |
list[T] |
List T — both immutable-by-default conceptually. Pythonic .append in a loop → build via :: then reverse, or fold directly. |
dict[K,V] |
Std.HashMap K V or K → Option V function — the function form proves better |
tuple |
Prod (×) for pairs; anonymous structure for n-tuples |
None / Optional[T] |
Option T — direct |
for x in xs: |
xs.foldl, xs.map, or explicit recursion — same as C→Lean |
| List comprehension | xs.filter p |>.map f — reads almost the same |
range(n) |
List.range n : List Nat |
f-string / str |
String — but if you're proving things about strings, use List Char for induction |
@dataclass |
structure — direct |
raise / try |
Except ε α monad — or precondition the error away |