Skip to content

Rename monoid-related operational typeclass instances to include the suffix '_instance'

Ralf Jung requested to merge ralf/op_instance_names into master

This was done using the following sed script:

sed -i -E 's/Instance ([a-zA-Z0-9_]+)( .*: (Op|P?Core|ValidN?|Unit) )/Instance \1_instance\2/' $(find iris/algebra -name "*.v")

Some manual fixup was needed; see the second commit for that. We might want to do something about some of these proofs?

This rename opens the opportunity of renaming lemmas such as frac_valid' to remove the ' that makes no sense here.

Merge request reports