Documentation

VCVio.EvalDist.Defs.Support.Failure

Operational failure #

HasEvalSet.LawfulFailure states that failure has no possible outputs under MonadAttach. The laws concern operational outputs independently of any probability interpretation.

source
class HasEvalSet.LawfulFailure (m : Type u → Type v) [Alternative m] [MonadAttach m] :
Prop

Failure has no possible outputs under monadic attachment.

Instances
    source
    @[simp]
    theorem support_failure {m : Type u → Type v} [Alternative m] [MonadAttach m] [HasEvalSet.LawfulFailure m] {α : Type u} :
    support failure = ∅

    Failure has no possible outputs.

    source
    @[simp]
    theorem finSupport_failure {m : Type u → Type v} [Alternative m] [MonadAttach m] [HasEvalSet.LawfulFailure m] {α : Type u} [HasEvalFinset m] [DecidableEq α] :
    finSupport failure = ∅

    Failure has empty finite support.

    source
    instance OptionT.instLawfulFailure (m : Type u → Type v) [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
    HasEvalSet.LawfulFailure (OptionT m)

    Optional failure has no possible outputs when attachment respects pure computations.