pith. machine review for the scientific record. sign in
def definition def or abbrev

apply

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  42noncomputable def apply {α β : Type} (A : Alignment α β) (m : Measurement α) : Measurement β :=

proof body

Definition body.

  43  { value := A.map m.value
  44    window := m.window
  45    protocol := A.protocol.protocol
  46    uncertainty := m.uncertainty
  47    notes := m.notes ++ [s!"Aligned via {A.protocol.name}"]
  48  }
  49
  50end Alignment
  51
  52end RSNative
  53end Measurement
  54end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.