As a clarification, I do not quite agree on that we cannot express pop_many in Pyre, it should be so simple as to write:

def pop_many(xs: SizedList[T, M], n: N) -> SizedList[T, M - N]: ...

Or in current prefix syntax:

def pop_many(xs: SizedList[T, M], n: N) -> SizedList[T, Add[M,Mult[N,Literal[-1]]]: ...

Best,
Alfonso.
_______________________________________________
Typing-sig mailing list -- typing-sig@python.org
To unsubscribe send an email to typing-sig-leave@python.org
https://mail.python.org/mailman3/lists/typing-sig.python.org/
Member address: n.a.sobolev@gmail.com