def definition def or abbrev

`init`

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

formal statement (Lean)

  31@[simp] def init (reg6 : Reg6) (aux5 : Aux5) : LState :=

proof body

Definition body.

  32  let base := LNAL.LState.init reg6 aux5
  33  { base := base, windowIdx := 0, winJ := 0, winJPrev := 0 }
  34
  35/-- Detect if the current window budget has been depleted. -/

used by (9)

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

voxelStep in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
knownParity_eq_parityOf_known' in IndisputableMonolith.Complexity.SAT.Backprop decl_use
AllReachable in IndisputableMonolith.Complexity.SAT.Completeness decl_use
IsolationInvariant in IndisputableMonolith.Complexity.SAT.Completeness decl_use
Reachable in IndisputableMonolith.Complexity.SAT.Completeness decl_use
foldl_xor_init in IndisputableMonolith.Complexity.SAT.XOR decl_use
parityOf_singleton in IndisputableMonolith.Complexity.SAT.XOR decl_use
foldl_add_eq_sum in IndisputableMonolith.Modal.Actualization decl_use
mockState in IndisputableMonolith.VM.Commit decl_use

depends on (2)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
LState in IndisputableMonolith.VM.State decl_use