def definition def or abbrev

`actionCost_decidable`

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

formal statement (Lean)

 144def actionCost_decidable (a b : ActionState) : Decidable (a = b) :=

Definition body.

 145  inferInstance
 146

Lean names referenced from this declaration's body.

ActionState in IndisputableMonolith.Foundation.UniversalForcing.Strict.Ethics decl_use