Zulip Chat Archive

Stream: std4

Topic: Deque

James Gallicchio (Jul 16 2023 at 23:37):

I don't see an implementation of the standard amortized O(1) deque (two lists, one reversed) anywhere, should I PR one?

James Gallicchio (Jul 16 2023 at 23:38):

(And does someone already have an implementation with proper lemmas and such?

James Gallicchio (Jul 17 2023 at 00:10):

Okay, I started implementing one and it's somewhat unclear whether I should quotient by the equivalence relation. I suspect I should not.

François G. Dorais (Jul 17 2023 at 04:43):

This should be PR to Std4, just like any of the standard textbook data structures. Correctness proofs can follow later, I think, but they are not that hard in this case. I think this should go in Std/Data/List/Deque.lean but I'm not sure.

James Gallicchio (Jul 17 2023 at 04:52):

Just gonna call it Std.Deque in Std/Data/Deque.lean.

James Gallicchio (Jul 17 2023 at 04:52):

hmm, although you're right that it's not the best deque impl.

Mario Carneiro (Jul 17 2023 at 12:43):

There is Init.Data.Queue already

James Gallicchio (Jul 17 2023 at 15:31):

aha :) I knew it'd be somewhere. sorry for the noise!

Last updated: Dec 20 2023 at 11:08 UTC