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)
27structure SpatialSemantics where
28 step : IndisputableMonolith.LNAL.LProgram → LNALField → LNALField
29
30namespace SpatialSemantics
31
32/-- Iterate `step` for `n` steps (functional execution). -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
RSNSBridgeSpec
in IndisputableMonolith.ClassicalBridge.Fluids.Bridge
decl_use
-
run
in IndisputableMonolith.ClassicalBridge.Fluids.LNAL
decl_use
-
independent
in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
decl_use
depends on (3)
Lean names referenced from this declaration's body.
-
LNALField
in IndisputableMonolith.ClassicalBridge.Fluids.LNAL
decl_use
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use