This PR starts using the opaque feature of Agda 2.6.4 in the cubical library. Namely, it replaces the old abstract keyword in QuotientAlgebra.agda (where it was used to keep type checking times reasonable) with the new opaque/unfolding mechanism. I think the result is much cleaner and more readable than the old huge abstract block. (And also we could now use named modules again if we wanted!)
The transformation was straight-forward, none of the actual definitions had to be changed at all. (I only had to indent them one more level...)
I made a separate opaque block for every definition. This is I think recommendable because the way that definitions in the same opaque block can only be unfolded together can be confusing.
I am planning to do the same in FPAlgebra.agda, but thought it is good to start with small steps. :-)
This PR starts using the
opaque
feature of Agda 2.6.4 in the cubical library. Namely, it replaces the oldabstract
keyword inQuotientAlgebra.agda
(where it was used to keep type checking times reasonable) with the newopaque
/unfolding
mechanism. I think the result is much cleaner and more readable than the old hugeabstract
block. (And also we could now use named modules again if we wanted!)The transformation was straight-forward, none of the actual definitions had to be changed at all. (I only had to indent them one more level...)
I made a separate
opaque
block for every definition. This is I think recommendable because the way that definitions in the sameopaque
block can only be unfolded together can be confusing.I am planning to do the same in
FPAlgebra.agda
, but thought it is good to start with small steps. :-)