Mentions légales du service

Skip to content

Banker's Queue, verified

Armaël Guéneau requested to merge bankersQueue into master

Remaining cleanup TODOs:

  • in Streams.v, some lemmas about the previous definition of subdebits are commented out. They should be either deleted or revived (but they were not used in any case)
  • some tactic helpers are duplicated between Streams.v and bqueue/Proof.v, they need to be factored out in some way or another.
Edited by Armaël Guéneau

Merge request reports