RosettaCodeData/Task/Queue-Definition/V/queue-definition-1.v
2023-07-01 13:44:08 -04:00

4 lines
108 B
Coq

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