Skip to content

Typed prophecy variables + cleanup

Rodolphe Lepigre requested to merge lepigre/examples:typed_proph into master

This MR introduces the following changes:

  • new folders theories/proph and theories/proph/lib,
  • things unrelated to logical atomicity moved from theories/logatom to the new folders,
  • a more complete typed prophecy interface (supporting one-shot prophecies) that is now usable,
  • examples using the typed prophecy interface (lazy coin + clairvoyant coin),
  • specs for all the coin examples, eager implementation for the eager spec.

@jung: the coin examples of the Iris repository are included in a modified version, mainly linking them to their spec.

Merge request reports