Precomposition spectrum: applying a function before building a spectrum
Also requires removing lift_compose as it does not hold for this spectrum
Showing
- current-formalism/Core/RobotInfo.v 5 additions, 6 deletionscurrent-formalism/Core/RobotInfo.v
- current-formalism/Gathering/InR2/Algorithm.v 2 additions, 2 deletionscurrent-formalism/Gathering/InR2/Algorithm.v
- current-formalism/Gathering/InR2/FSyncFlexNoMultAlgorithm.v 10 additions, 8 deletionscurrent-formalism/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
- current-formalism/Gathering/InR2/Peleg.v 8 additions, 6 deletionscurrent-formalism/Gathering/InR2/Peleg.v
- current-formalism/Spectra/PreCompositionSpectrum.v 53 additions, 0 deletionscurrent-formalism/Spectra/PreCompositionSpectrum.v
- current-formalism/Util/Preliminary.v 12 additions, 0 deletionscurrent-formalism/Util/Preliminary.v
- current-formalism/_CoqProject 1 addition, 0 deletionscurrent-formalism/_CoqProject
Loading
Please register or sign in to comment