Observable

formal source

 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⟩⟩
 176instance (U : Type) : Sub (Quantity U) := ⟨fun a b => ⟨a.val - b.val⟩⟩
 177instance (U : Type) : Neg (Quantity U) := ⟨fun a => ⟨-a.val⟩⟩
 178instance (U : Type) : SMul ℝ (Quantity U) := ⟨fun r a => ⟨r * a.val⟩⟩
 179
 180@[simp] theorem val_zero (U : Type) : (0 : Quantity U).val = 0 := rfl
 181@[simp] theorem val_add {U : Type} (a b : Quantity U) : (a + b).val = a.val + b.val := rfl
 182@[simp] theorem val_sub {U : Type} (a b : Quantity U) : (a - b).val = a.val - b.val := rfl
 183@[simp] theorem val_neg {U : Type} (a : Quantity U) : (-a).val = -a.val := rfl
 184@[simp] theorem val_smul {U : Type} (r : ℝ) (a : Quantity U) : (r • a).val = r * a.val := rfl
 185
 186end Quantity
 187
 188/-! ### Unit/semantic tags (empty types) -/
 189
 190inductive TickUnit : Type
 191inductive VoxelUnit : Type
 192inductive CohUnit : Type