2 lines
83 B
Coq
2 lines
83 B
Coq
|
[seq [] swap dup [zero? not] [rolldown [dup] dip cons rollup pred] while pop pop].
|