structure
definition
Ledger
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 67.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
64/-! ## Full Ledger -/
65
66/-- A ledger: a sequence of transactions that globally balance. -/
67structure Ledger where
68 /-- The transactions in the ledger. -/
69 transactions : List Transaction
70 /-- Total debit. -/
71 total_debit : ℤ := (transactions.map (·.debit)).sum
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. -/
80def empty : Ledger := {
81 transactions := [],
82 total_debit := 0,
83 total_credit := 0,
84 global_balance := by omega
85}
86
87/-- A singleton ledger. -/
88def singleton (t : Transaction) : Ledger := {
89 transactions := [t],
90 total_debit := t.debit,
91 total_credit := t.credit,
92 global_balance := t.balanced
93}
94
95/-- Append a transaction to a ledger. -/
96def append (L : Ledger) (t : Transaction) : Ledger := {
97 transactions := L.transactions ++ [t],