9 lines
210 B
Coq
9 lines
210 B
Coq
|
[comb
|
||
|
|
[2dup [a b : a b a b] view].
|
||
|
|
[2pop pop pop].
|
||
|
|
|
||
|
|
[ [pop zero?] [2pop [[]]]
|
||
|
|
[null?] [2pop []]
|
||
|
|
[true] [2dup [pred] dip uncons swapd comb [cons] map popd rollup rest comb concat]
|
||
|
|
] when].
|