Documentation

VCVio.EvalDist.Instances.FinRatPMF

EvalDist Instances for FinRatPMF.Raw #

This file exposes the executable FinRatPMF.Raw monad to the generic EvalDist API.

source
@[implicit_reducible]
noncomputable instance FinRatPMF.Raw.instHasEvalPMF :
HasEvalPMF Raw
source
@[implicit_reducible]
instance FinRatPMF.Raw.instHasEvalFinset :
HasEvalFinset Raw
source
@[simp]
theorem FinRatPMF.Raw.finSupport_eq_support {α : Type u} [DecidableEq α] (mx : Raw α) :
finSupport mx = mx.support