CHANGELOG.md · 5e346fc58959c3225a7fabdbd62a39c554104065 · William Mansky / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

3 years ago

big_op: weaken all Absorbing conditions using TCOr and Affine · 5e346fc5

Glen Mével authored 3 years ago

For all big_op lemmas which had an `Absorbing` condition, the condition
has now become an alternative between `Affine` and `Absorbing`. Thus the
lemmas are made more general. This change is spreading the use of the
`TCOr (Affine _) (Absorbing _)` pattern.

5e346fc5

big_op: weaken all Absorbing conditions using TCOr and Affine

Glen Mével authored 3 years ago

For all big_op lemmas which had an `Absorbing` condition, the condition
has now become an alternative between `Affine` and `Absorbing`. Thus the
lemmas are made more general. This change is spreading the use of the
`TCOr (Affine _) (Absorbing _)` pattern.

To find the state of this project's repository at the time of any of these versions, check out the tags.