pith. machine review for the scientific record. sign in
structure definition def or abbrev

Ledger

show as:
view Lean formalization →

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)

  67structure Ledger where
  68  /-- The transactions in the ledger. -/
  69  transactions : List Transaction
  70  /-- Total debit. -/
  71  total_debit : ℤ := (transactions.map (·.debit)).sum

proof body

Definition body.

  72  /-- Total credit. -/
  73  total_credit : ℤ := (transactions.map (·.credit)).sum
  74  /-- Global balance: total debit + total credit = 0. -/
  75  global_balance : total_debit + total_credit = 0
  76
  77namespace Ledger
  78
  79/-- The empty ledger. -/

depends on (5)

Lean names referenced from this declaration's body.