Skip to content

Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type.

Jacques-Henri Jourdan requested to merge jh/infinite_function_cmra into master

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Merge request reports