Sept. 23, 2020
1:44 p.m.
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.