Skip to content

provide big_op lemmas outside of bi module

Ralf Jung requested to merge ralf/bigop into gen_proofmode

I squashed the LambdaRust port to see what the diff looks like, and the big-op-related changes really stand out. I don't see a good reason to break compatibility this way, given there's a very low risk of these conflicting with Coq's standard library and given that we don't put the updates and plainly into the bi module either.

This changes the diffstat on LambdaRust from "225 insertions(+), 261 deletions(-)" to "128 insertions(+), 164 deletions(-)". Looking over it, I don't see any obvious low-hanging fruit left.

For now, I left the option of using the big op lemmas from inside the bi module to maintain compatibility with developments that use it that way.

Edited by Ralf Jung

Merge request reports