affeldt-aist
commented
1 year ago @t6s
I made a few edits in the doc/code base on the following observations:
in necset.v:
- biglubDr_semiLattConvType appears in the doc but not in the code
- necset_semiCompSemiLattType, necset_semiCompSemiLattConvType do not appear explicitly in the code anymore
- necset_convType still appears but is maybe not needed
in convex.v:
- R_orderedConvType, fun_orderedConvType, oppConvType do not appear explicitly in the code anymore
Can you check whether we can improve things a bit in those files while changes are still fresh in our memories? (Keeping in mind that the following PR is building on convex.v: https://github.com/affeldt-aist/infotheo/pull/85 ) @Tragicus
t6s
@t6s Tentative move of morphisms to HB, but this change has not yet been tested with monae.