mapWithProtocol

formal source

 133  }
 134
 135/-- Map the value and replace protocol (e.g., when you derive a new observable). -/
 136def mapWithProtocol {α β : Type} (f : α → β) (p : Protocol) (m : Measurement α) : Measurement β :=
 137  { value := f m.value
 138    window := m.window
 139    protocol := p
 140    uncertainty := m.uncertainty
 141    notes := m.notes
 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. -/