"global" hybrid theory, plus two examples

[alleystoughton]

Added "step" hybrid theory, plus two examples. (Currently in temp directory in theories.)

[fdupress]

Thank you. Some comments.

Not approving yet because the examples are definitely not in the right place.

[alleystoughton]

I put GlobalHybrid.ec in theories/crypto.

[fdupress]

Would be nice to have the existing hybrid refactored as an instance of this (in particular, avoiding repeating the proof for the telescoping sums), but this is fine to merge as it is.

[fdupress]

Oh, sorry; not quite.

Please edit the commit message.

Something along the lines of

[theories/crypto] global hybrid theory

This adds a theory for hybrid arguments where the entire
experiment is parameterised, and two examples of how to
use it.

[fdupress]

Generally, keeping the first line under 52 characters to indicate the "what", leaving a blank line, and keeping further lines under 80 characters to indicate the "why" is good practice.

Most people interact with git through the CLI client, which makes assumptions about commit messages and their formatting when displaying them. (Which are repeated in the github UI, hence why your commit titles get truncated after 52 characters.)

[alleystoughton]

Would be nice to have the existing hybrid refactored as an instance of this (in particular, avoiding repeating the proof for the telescoping sums), but this is fine to merge as it is.

I can have a go this coming summer, if no-one gets to it before then.

[alleystoughton]

Oh, sorry; not quite.

Please edit the commit message.

Something along the lines of

[theories/crypto] global hybrid theory

This adds a theory for hybrid arguments where the entire
experiment is parameterised, and two examples of how to
use it.

I changed the commit message, via git. Was there a way for me to do this without restarting all the checks?

[fdupress]

No, but this is alright. I'll set auto-merge so this merges as soon as the checks succeed.