structure definition def or abbrev

`ProgramSpec`

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

formal statement (Lean)

  29structure ProgramSpec where
  30  combination : CombinationID
  31  protocol : ProtocolSpec
  32  priority : Priority
  33  action : AnalysisAction
  34  deliverable : Deliverable
  35  pipeline : PipelineSpec
  36  ready : EmpiricallyReady combination
  37
  38/-- Program row assigned to an implemented Option A combination. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

firstPassProgram in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
programSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
programSpec_injective in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use

depends on (11)

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
AnalysisAction in IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan decl_use
Deliverable in IndisputableMonolith.Foundation.OptionAEmpiricalDeliverables decl_use
PipelineSpec in IndisputableMonolith.Foundation.OptionAEmpiricalPipeline decl_use
ProtocolSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
Priority in IndisputableMonolith.Foundation.OptionAEmpiricalQueue decl_use
EmpiricallyReady in IndisputableMonolith.Foundation.OptionAEmpiricalReadiness decl_use
CombinationID in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
row in IndisputableMonolith.YM.Dobrushin decl_use