Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
Compare
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type.
Jacques-Henri Jourdan authored 
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.
fa897ff5
History
user avatar fa897ff5
History
Name Last commit Last update