mapUncertainty

formal source

 142  }
 143
 144/-- Transform the uncertainty record (when present). -/
 145def mapUncertainty {α : Type} (uMap : Uncertainty → Uncertainty) (m : Measurement α) : Measurement α :=
 146  { value := m.value
 147    window := m.window
 148    protocol := m.protocol
 149    uncertainty := m.uncertainty.map uMap
 150    notes := m.notes
 151  }
 152
 153def addNote {α : Type} (note : String) (m : Measurement α) : Measurement α :=
 154  { m with notes := m.notes ++ [note] }
 155
 156def addNotes {α : Type} (notes : List String) (m : Measurement α) : Measurement α :=
 157  { m with notes := m.notes ++ notes }
 158
 159end Measurement
 160
 161/-- An observable extracts a `Measurement α` from some state type `S`. -/
 162abbrev Observable (S α : Type) : Type := S → Measurement α
 163
 164/-! ## Tagged quantities (type-safe units) -/
 165
 166/-- A real-valued quantity tagged with a unit/semantic label. -/
 167structure Quantity (U : Type) where
 168  val : ℝ
 169
 170instance (U : Type) : CoeTC (Quantity U) ℝ := ⟨Quantity.val⟩
 171
 172namespace Quantity
 173
 174instance (U : Type) : Zero (Quantity U) := ⟨⟨0⟩⟩
 175instance (U : Type) : Add (Quantity U) := ⟨fun a b => ⟨a.val + b.val⟩⟩