`SpatialSemantics`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.LNAL
domain: ClassicalBridge
line: 27 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.LNAL on GitHub at line 27.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  24abbrev LNALField : Type := Array LNALVoxel
  25
  26/-- A minimal interface for spatial execution of an LNAL program over a field of voxels. -/
  27structure SpatialSemantics where
  28  step : IndisputableMonolith.LNAL.LProgram → LNALField → LNALField
  29
  30namespace SpatialSemantics
  31
  32/-- Iterate `step` for `n` steps (functional execution). -/
  33def run (sem : SpatialSemantics) (P : IndisputableMonolith.LNAL.LProgram) : LNALField → Nat → LNALField
  34  | s, 0 => s
  35  | s, Nat.succ n => run sem P (sem.step P s) n
  36
  37end SpatialSemantics
  38
  39end Fluids
  40end ClassicalBridge
  41end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.