Skip to content

GitLab

Move big-op instances up.

Merged Robbert Krebbers requested to merge robbert/big_op_instances.v into master

This moves the instances for Affine/Timeless/etc up, so they are just below the Proper instances.

This is useful because other (future) lemmas in the file can make use of them.