Various measure set operations (Figure 12)

ink

def MeasureSet.lift {α : Type} (f : Meas → Meas) : MeasureSet → MeasureSet

• lift;

Equations

• MeasureSet.lift f x = match x with | MeasureSet.tainted m => MeasureSet.tainted (f m) | MeasureSet.set ms h => MeasureSet.set (List.map f ms) (_ : ¬List.map f ms = [])

ink

def MeasureSet.taint {α : Type} : MeasureSet → MeasureSet

• taint; and

Equations

• MeasureSet.taint x = match x with | MeasureSet.tainted m => MeasureSet.tainted m | MeasureSet.set ms h => MeasureSet.tainted (List.head ms h)

ink

def MeasureSet.union {α : Type} (F : Factory α) : MeasureSet → MeasureSet → MeasureSet

• union (⊎)

Equations

• One or more equations did not get rendered due to their size.