Started implementation of Giry monad - #1608

Merged

affeldt-aist merged 14 commits into

math-comp:masterfrom

alejandroag:giry-impl

Dec 3, 2025

Commits on Nov 22, 2025

Started implementation of Giry monad

alejandroag
authored and
affeldt-aist
committed
53dc49a
use existing facilities
affeldt-aist
committed
2f8b32d
measurable_setI was measurableI
affeldt-aist
committed
c3cd60e
more idiomatic use of library
affeldt-aist
committed
35b8b0b
minor cleaning in proofs marked as TODOs
affeldt-aist
committed
4f8c40e
just rebase and lint
affeldt-aist
committed
8f5ae95
naming convention
affeldt-aist
committed
77c3d46
add to makefiles
affeldt-aist
committed
f8052ce
changelog, doc until measurable_giry_int
affeldt-aist
committed
58f6efa

Commits on Nov 23, 2025

doc until giry_join
affeldt-aist
committed
af7caeb

Commits on Nov 24, 2025

mv lemmas
affeldt-aist
committed
76e16d3
fix
affeldt-aist
committed
7702034
fix
affeldt-aist
committed
877115b
fix
affeldt-aist
committed
53310e1