def definition def or abbrev

`addNotes`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 156def addNotes {α : Type} (notes : List String) (m : Measurement α) : Measurement α :=

proof body

Definition body.

 157  { m with notes := m.notes ++ notes }
 158
 159end Measurement
 160
 161/-- An observable extracts a `Measurement α` from some state type `S`. -/

depends on (5)

Lean names referenced from this declaration's body.

Measurement in IndisputableMonolith.Data.Import decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use