structure definition def or abbrev

`Ledger`

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

formal statement (Lean)

  34structure Ledger (M : RecognitionStructure) where
  35  debit : M.U → ℤ
  36  credit : M.U → ℤ
  37

Lean names referenced from this declaration's body.

RecognitionStructure in IndisputableMonolith.Chain decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
RecognitionStructure in IndisputableMonolith.Foundation.RecognitionForcing decl_use
M in IndisputableMonolith.Recognition decl_use
RecognitionStructure in IndisputableMonolith.Recognition decl_use
U in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
RecognitionStructure in IndisputableMonolith.RRF.Core.Recognition decl_use
RecognitionStructure in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use