Successful-output measure of failure

LawfulFailureEvalDistSemantics certifies that failure has zero successful-output measure. This law is independent of attachment, pure, bind, and any discrete probability representation.

class LawfulFailureEvalDistSemantics (m : Type u → Type v) [Alternative m] [EvalDistSemantics m] : Prop

A measure interpretation assigns zero successful-output mass to failure.

• denote_failure {α : Type u} [MeasurableSpace α] : 𝒟[failure] = 0

  Failure denotes the zero measure.

@[simp]

theorem evalDist_failure_eq_zero {m : Type u → Type v} [Alternative m] [EvalDistSemantics m] [LawfulFailureEvalDistSemantics m] {α : Type u} [MeasurableSpace α] : 𝒟[failure] = 0

Failure has zero successful-output measure.