def
definition
fullSafety
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Superhuman.TechnologicalAccess on GitHub at line 112.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
109 has_deterministic_shutdown = true
110
111/-- The canonical safety configuration. -/
112def fullSafety : SafetyRequirements where
113 has_watchdog := true
114 has_overcurrent_protection := true
115 has_overvoltage_protection := true
116 has_thermal_protection := true
117 has_loss_of_load_detection := true
118 has_deterministic_shutdown := true
119 all_satisfied := ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
120
121end IndisputableMonolith.Superhuman.TechnologicalAccess