RosettaCodeData/Task/Queue-Definition/V/queue-definition-1.v

5 lines
108 B
Coq

[fifo_create []].
[fifo_push swap cons].
[fifo_pop [[*rest a] : [*rest] a] view].
[fifo_empty? dup empty?].