Probability Distributions on Potentially Failing Computations #
This file gives an instance to extend a evalDist instance on a monad to one transformed by
the OptionT monad transformer.
dt: should add more instances and connecting lemmas
Standalone HasEvalSet (OptionT m) instance under the weaker [HasEvalSet m] assumption.
This is deliberately kept separate from the HasEvalSPMF (OptionT m) instance below, which
re-exports the same toSet to make the resulting typeclass diamond definitionally equal.
Keeping this standalone instance means support on OptionT m works without requiring a
full HasEvalSPMF m — only HasEvalSet m is needed (e.g., for support_liftM).
Lift a HasEvalFinset instance to OptionT. by just taking preimage under some.
Lift a HasEvalSPMF m instance to HasEvalSPMF (OptionT m).
Note: a more specific HasEvalPMF m → HasEvalSPMF (OptionT m) path would make explicit
that failure comes solely from OptionT, but this general instance subsumes it.
Lean 4 automatically synthesizes toSet from the standalone HasEvalSet (OptionT m) instance
above, ensuring the diamond is definitionally equal (per Mathlib convention). The support_eq
field then serves as the coherence proof between the set-path and distribution-path.