Repository navigation

feat(PFunctor): measure semantics for free monads and resumptions - #1089

Open

dtumad wants to merge 6 commits into

leanprover:mainfrom

dtumad:dtumad/pfunctor-measure

Commits on Oct 5, 2026

feat(PFunctor): relate W-types, M-types and free monads

dtumad
and
claude
committed
90278e5
refactor(PFunctor): build polynomial objects with `Obj.mk`

dtumad
and
claude
committed
e991370
feat(PFunctor): add coinductive resumptions

dtumad
and
claude
committed
90e958b
refactor(Resumption): mirror the polynomial free monad API

dtumad
and
claude
committed
0d4434c
feat(PFunctor): relate M-types and never-returning resumptions

dtumad
and
claude
committed
316d261

Commits on Oct 6, 2026

feat(PFunctor): measure semantics for free monads and resumptions

dtumad
and
claude
committed
2f373a6