Luc Duponcheel

Hello Rob23oba and zwarich, So what's the conclusion? Changing the code of `Task.bind` so that it does not allow delaying creating lambdas)? How did it work before the `nightly-2025-06-21` build?...

Hello Rob23oba and zwarich, Maybe I exaggerated a bit by writing that only a `Task.seq` is needed *in general*. For my *specific* use case, parallel program combination, `Task.seq` suffices.

Rob23oba, great, using your suggestion it works with `leanprover/lean4:nightly-2025-06-20` and `leanprover/lean4:nightly-2025-06-21` but not with`leanprover/lean4:nightly-2025-06-22` ... (???) ...

Hello Rob23oba and zwarich, good news, using `abbrev` (to *really* be sure that we are dealing with a function) as in ```lean abbrev computationValuedFunction (computation : Type → Type) (α...

Rob23oba, I tried `def` with the `stable` version myself and it worked! thx!! Why would `abbrev` cause problems later? `abbrev` simply defines `computationValuedFunction computation α β` as a synonym of...

fair enough I am busy now converting the code of my `PSBP` library https://github.com/LucDuponcheelAtGitHub. the impact on the `MWE` was minimal, but `PSBP` (which can be seen as a programming...

Updating may code base (almost mechanically) results in type ambiguity errors like ``` Ambiguous term αpγ >=> γpδ Possible interpretations: αpγ >=> γpδ : computationValuedFunction computation α δ αpγ >=>...

Rob23oba, I am going to present a new MWE asap where the type issues occur (but there are only 24 hours in a day). I will try to solve the...

Rob23oba, as far as trying to produce a MWE, your ```lean macro_rules | `($_ >=> $_) => Lean.Macro.throwError "disabled" infixl:55 " >=> " => andThenP ``` suggestion solved the issue....

Rob23oba, my whole codebase has been refactored, using your suggestion ```lean macro_rules | `($_ >=> $_) => Lean.Macro.throwError "disabled" ``` thx now I need to sync the documentation Frankly, without...