Bas Spitters

Talking to @alejandroag, his Giry monad may be more complex than what we need. Perhaps it is better to port the existing formalization of distributions to the std reals.

I understand that the "experimental reals" are deprecated in MC. So, I guess there is a porting effort in MCA. @affeldt-aist, @hoheinzollern could you enlighten us about the plans, and...

Thanks @affeldt-aist @strub that clarifies the situation and gives a good way forward. @alejandroag how do your plans with the Giry monad compare with the plans of @strub ?

Just to clarify, we would like to continue to use the discrete probabilities (distr) in SSProve, but with @MarkusKL we would sleep better if the admitted lemmas were proven. Which...

@CohenCyril, @arthuraa Do you have any input on this? Should these lemmas be moved/ported to finmap? https://github.com/arthuraa/extructures/issues/22 We can probably also upstream any utility libraries we create around this. e.g....

@MarkusKL Maybe you can give an overview here of your additions to finmap.

Thanks @CohenCyril . FYI, we're trying to integrate @MarkusKL nominal-SSProve into the main repo. Maybe there's a possibility to refactor more to be inline with your work? github.com/MarkusKL/nominal-ssprove/blob/master/theories/Nominal.v There's also...

@CohenCyril What are the plans on nominal Rocq. Will it be moved to Rocq community? We can probably integrate @MarkusKL code into a joint library.

@CohenCyril Nominal SSProve has now been merged. Would it make sense to move the general nominal part to a more general place?

@MarkusKL what is the status of this, now that nominal has been merged?