feat: add a predicate for monad morphisms - #856

Merged

fmontesi merged 27 commits into

leanprover:mainfrom

eric-wieser:monadHom

Sep 12, 2026

Commits on Sep 2, 2026

feat: add a predicate for monad morphisms
eric-wieser
committed
2798f88
drop dcomp
eric-wieser
committed
050995d
section
eric-wieser
committed
f9eec96
wp
eric-wieser
committed
a522805
Close the proof_wanted
eric-wieser
committed
87da9b3
remove grind
eric-wieser
committed
75b9bd2

Commits on Sep 3, 2026

feat: add monad-polymorphic sorts
eric-wieser
committed
9b8ed4e
drop merge
eric-wieser
committed
e4b031e
imports
eric-wieser
committed
5576d8b

Commits on Sep 4, 2026

Address the TODO
eric-wieser
committed
fd34ff1

Commits on Sep 6, 2026

Fix lint
eric-wieser
authored
715b668
lint fix
eric-wieser
authored
ba1178b
Update Cslib/Algorithms/Lean/Sort/Merge.lean

eric-wieser
and
fmontesi
authored
e013611

Commits on Sep 9, 2026

review comments
eric-wieser
committed
8e0c1a9
Merge branch 'eric-wieser/mergeM' of github.com:eric-wieser/cslib into eric-wieser/mergeM
eric-wieser
committed
014bd47
Update Cslib/Algorithms/Lean/Sort/Insertion.lean

eric-wieser
and
kim-em
authored
ff566e0
generalize universes
eric-wieser
committed
bd9edd2
more review comments
eric-wieser
committed
b69ee6b
drop lawful
eric-wieser
committed
445d6bd

Commits on Sep 10, 2026

fix namespace
eric-wieser
committed
9025e64
add simp lemmas
eric-wieser
committed
1a1e327
Merge branch 'eric-wieser/mergeM' into monadHom
eric-wieser
committed
21b3f3c
add IsMonadHom uses
eric-wieser
committed
fff58b1
ret is a monad hom
eric-wieser
committed
0002400
Merge remote-tracking branch 'origin/main' into monadHom
eric-wieser
committed
47aa94c
and insertionSort
eric-wieser
committed
94497e1
fix name
eric-wieser
committed
386d4af