No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
28inductive FailureMode where
29 | yielding | buckling | fatigue | fracture | creep
30 deriving DecidableEq, Repr, BEq, Fintype
31
used by (15)
From the project-wide theorem graph. These declarations reference this one in their body.
-
failureModeCount
in IndisputableMonolith.Engineering.StructuralSafetyFromJCost
decl_use
-
StructuralSafetyCert
in IndisputableMonolith.Engineering.StructuralSafetyFromJCost
decl_use
-
ProtocolFalsifiable
in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol
decl_use
-
ProtocolSpec
in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol
decl_use
-
failureMode
in IndisputableMonolith.Foundation.OptionAFalsifierRegistry
decl_use
-
FailureMode
in IndisputableMonolith.Foundation.OptionAFalsifierRegistry
decl_use
-
failureMode_count
in IndisputableMonolith.Foundation.OptionAFalsifierRegistry
decl_use
-
FalsifierRegistryCert
in IndisputableMonolith.Foundation.OptionAFalsifierRegistry
decl_use
-
FailureMode
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
failureModeCount
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
GovernanceCert
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
institutionFailureMode
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
FailureMode
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use
-
failureModeCount
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use
-
FatigueFractureCert
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use
depends on (3)
Lean names referenced from this declaration's body.
-
FailureMode
in IndisputableMonolith.Foundation.OptionAFalsifierRegistry
decl_use
-
FailureMode
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
FailureMode
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use