changelog constructive_ereal.v

CHANGELOG_UNRELEASED.md

@@ -17,6 +17,17 @@
   + definition `convex_lmodType` with instances using `Choice.on` and `isConvexSpace.Build`
   + definition `convex_realDomainType` with instance using `isConvexSpace.Build`
 
+- in `constructive_ereal.v`:
+  + definition `dEFin`
+  + notations `%:dE`, `%:E` (`ereal_dual_scope`)
+  + notation `\bar^d ...` (`type_scope`) for dual extended real numbers
+  + instance using `isNmodule.Build` for `\bar`
+  + instances using `Choice.on` and `isNmodule.Build` for `\bar^d`
+  + lemma `EFin_semi_additive`
+  + lemmas `dEFinE`, `dEFin_semi_additive`
+  + instance using `isSemiAdditive.Build` for `\bar^d`
+  + canonical `dEFin_snum`
+
 ### Changed
 
 - in `boolp.v`:
@@ -121,6 +132,19 @@
 	+ in definition `tree_of` and lemma `cantor_like_finite_prod`:
 	  `pointed_discrete` -> `pointed_discrete_topology`
 
+- in `constructive_ereal.v`:
+  + definition `ereal_eqMixin` and canonical `ereal_eqType` -> instance using `hasDecEq.Build`
+  + definition `ereal_choiceMixin` and canonical `ereal_choiceType` -> instance using `Choice.copy`
+  + definition `ereal_countMixin` and `ereal_countType` -> instance using `PCanIsCountable`
+  + definition `ereal_porderMixin` and canonical `Choice.copy` -> instance using `isPOrder.Build`
+  + in lemma `le_total_ereal` : `le_total_ereal` -> `total`
+  + canonicals `ereal_latticeType`, `ereal_distrLatticeType`, `ereal_orderType`, `ereal_blatticeType`, `ereal_tblatticeType`, lemmas `ereal_blatticeMixin`, `ereal_blatticeMixin` ->
+    instances using `POrder_isTotal.Build`, `hasBottom.Build`, `hasTop.Build`
+  + canonicals `adde_monoid`, `adde_comoid`, `mule_mulmonoid` -> instance using `isMulLaw.Build`
+  + notations `maxe`, `mine`: `fun_scope` -> `function_scope`
+  + canonicals `mule_monoid`, `mule_comoid` -> instance using `isComLaw.Build`
+  + canonicals `maxe_monoid`, `maxe_comoid` -> instance using `isLaw.Build`
+
 ### Renamed
 
 ### Generalized
@@ -173,6 +197,10 @@
 - in `convex.v`:
   + field `convexspacechoiceclass`, canonicals `conv_eqType`, `conv_choiceType`, `conv_choiceType`
 
+- in `constructive_ereal.v`:
+  + canonicals `isLaw.Build`, `mine_comoid`
+
+
 ### Infrastructure
 
 ### Misc