def
definition
deferredTests
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalQueue on GitHub at line 100.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
97 [.c1CognitiveTensor, .c7UniversalResponse]
98
99/-- Deferred empirical tests. -/
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