Probability Distributions on Option return types

File for lemmas about evalDist on involving Option.

@[simp]

theorem probOutput_some_map_some {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α : Type u} (mx : m α) (x : α) : Pr[=some x | some <$> mx] = Pr[=x | mx]

theorem probOutput_some_map_none {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α : Type u} (mx : m α) : Pr[=none | some <$> mx] = 0