def definition def or abbrev

`isHighOrImmediate`

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

formal statement (Lean)

  47def isHighOrImmediate (c : CombinationID) : Prop :=

Definition body.

  48  empiricalPriority c = .immediate ∨ empiricalPriority c = .high
  49

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

EmpiricalProgramCert in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
FirstPassProgramComplete in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
firstPassProgram_exact_top_priority in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
EmpiricalQueueCert in IndisputableMonolith.Foundation.OptionAEmpiricalQueue decl_use
high_or_immediate_iff in IndisputableMonolith.Foundation.OptionAEmpiricalQueue decl_use
EmpiricalScheduleCert in IndisputableMonolith.Foundation.OptionAEmpiricalSchedule decl_use
firstPassSchedule_mem_high_or_immediate in IndisputableMonolith.Foundation.OptionAEmpiricalSchedule decl_use
firstPassSchedule_mem_iff_high_or_immediate in IndisputableMonolith.Foundation.OptionAEmpiricalSchedule decl_use

Lean names referenced from this declaration's body.

empiricalPriority in IndisputableMonolith.Foundation.OptionAEmpiricalQueue decl_use
CombinationID in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use