Evaluation Distributions of Computations with seq #
File for lemmas about evalDist and support involving the monadic seq, seqLeft,
and seqRight operations.
TODO: many lemmas should probably have mirrored versions for bind_map.
@[simp]
theorem
support_seq
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[HasEvalSet m]
[LawfulMonad m]
(mf : m (α → β))
(mx : m α)
:
@[simp]
theorem
finSupport_seq
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[HasEvalSet m]
[HasEvalFinset m]
[LawfulMonad m]
[DecidableEq (α → β)]
[DecidableEq α]
[DecidableEq β]
(mf : m (α → β))
(mx : m α)
:
@[simp]
theorem
evalDist_seq
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[HasEvalSPMF m]
[LawfulMonad m]
(mf : m (α → β))
(mx : m α)
: