Use Python's type variables
Why3's Python plugin uses the syntax 'foo
to denote type variables. But Python actually provides type variables, so it might be better to use them, rather than use our own incompatible syntax:
from typing import TypeVar
T = TypeVar('t')
def repeat(x: T, n: int) -> list[T]:
return [x]*n
The parser would have to explicitly recognize the statement ident = TypeVar(expr)
and register ident
as denoting a type variable. Another possibility would be to just disregard the statement and assume that any identifier not recognized as a type is a type variable.