xpile 0.1.615

Polyglot transpile workbench (Python/C/C++/Rust/Ruchy/Lean ↔ Rust/Ruchy/PTX/WGSL/SPIR-V) with provable contracts at every layer.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

from typing import Optional


def maybe(n: int) -> Optional[int]:
    if n > 0:
        return n
    return None


def sum_present(xs: list[Optional[int]]) -> int:
    # PMAT-887: the for-loop var `x` (Optional) is Some-narrowed inside the
    # `if x is not None:` body, so `total += x` unwraps. Was E0308 (the loop var
    # is prescan-mutable, which used to disqualify narrowing).
    total: int = 0
    for x in xs:
        if x is not None:
            total += x
    return total


def sum_truthy(xs: list[Optional[int]]) -> int:
    # `if x:` truthiness over an Optional loop var also narrows.
    total: int = 0
    for x in xs:
        if x:
            total += x
    return total