Repository navigation

feat(PFunctor): add resumptions and relate W-types, M-types and free monads - #1088

Open

dtumad wants to merge 5 commits into

leanprover:mainfrom

dtumad:dtumad/pfunctor-resumption

Open

feat(PFunctor): add resumptions and relate W-types, M-types and free monads#1088
dtumad wants to merge 5 commits into
leanprover:mainfrom
dtumad:dtumad/pfunctor-resumption

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