5 lines
108 B
Coq
5 lines
108 B
Coq
|
[fifo_create []].
|
||
|
|
[fifo_push swap cons].
|
||
|
|
[fifo_pop [[*rest a] : [*rest] a] view].
|
||
|
|
[fifo_empty? dup empty?].
|