Repository navigation

feat(PFunctor): add possible outputs and MonadAttach for free monads - #1087

Open

dtumad wants to merge 3 commits into

leanprover:mainfrom

dtumad:dtumad/freem-monad-attach

Commits on Oct 5, 2026

feat(PFunctor): add possible outputs and MonadAttach for free monads

dtumad
and
claude
committed
1902cfd
refactor(PFunctor): take the program first in `possibleOutputs`

dtumad
and
claude
committed
32fc333
feat(PFunctor): attach possible-output proofs through any handler

dtumad
and
claude
committed
4d38656