structure definition def or abbrev

`Neighborhood`

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

formal statement (Lean)

  58structure Neighborhood where
  59  left   : CellState
  60  center : CellState
  61  right  : CellState
  62
  63/-- Extract neighborhood from tape at position i -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

extractNeighborhood in IndisputableMonolith.Complexity.CellularAutomata decl_use
localRule in IndisputableMonolith.Complexity.CellularAutomata decl_use
Window in IndisputableMonolith.Complexity.CellularAutomata decl_use
LocalConfigSpace in IndisputableMonolith.RecogGeom.Locality decl_use
LocalConfigSpace in IndisputableMonolith.RecogGeom.Locality decl_use
locality_status in IndisputableMonolith.RecogGeom.Locality decl_use

depends on (3)

Lean names referenced from this declaration's body.

CellState in IndisputableMonolith.Complexity.CellularAutomata decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
neighborhood in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use