theorem
proved
immediateTests_length
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalQueue on GitHub at line 103.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
100def deferredTests : List CombinationID :=
101 [.c4QuantumMolecularDepth, .c6EriksonReverse]
102
103theorem immediateTests_length : immediateTests.length = 2 := by
104 decide
105
106theorem highPriorityTests_length : highPriorityTests.length = 3 := by
107 decide
108
109theorem mediumPriorityTests_length : mediumPriorityTests.length = 2 := by
110 decide
111
112theorem deferredTests_length : deferredTests.length = 2 := by
113 decide
114
115theorem immediateTests_nodup : immediateTests.Nodup := by
116 decide
117
118theorem highPriorityTests_nodup : highPriorityTests.Nodup := by
119 decide
120
121theorem mediumPriorityTests_nodup : mediumPriorityTests.Nodup := by
122 decide
123
124theorem deferredTests_nodup : deferredTests.Nodup := by
125 decide
126
127theorem immediateTests_exact (c : CombinationID) :
128 c ∈ immediateTests ↔ empiricalPriority c = .immediate := by
129 cases c <;> simp [immediateTests, empiricalPriority]
130
131theorem highPriorityTests_exact (c : CombinationID) :
132 c ∈ highPriorityTests ↔ empiricalPriority c = .high := by
133 cases c <;> simp [highPriorityTests, empiricalPriority]