def
definition
pathSpace_status
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Action.PathSpace on GitHub at line 161.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
158/-! ## Status report -/
159
160/-- Status string for the path-space module. -/
161def pathSpace_status : String :=
162 "Action.PathSpace: AdmissiblePath, actionJ, interp, fixedEndpoints (0 sorry, 0 axiom)"
163
164end Action
165end IndisputableMonolith