swaitsandClaude Opus 5.5
b0a9fd8ad4
The final month takes what the months before leave, spread over its days; a disposed asset stops on its disposal day. A skipped month is caught up in the month the run is made; a reversed run un-posts its month. New schedules spread by day; equal-months schedules must start on the 1st. Amounts round to the currency's own minor unit. Kani and Lean proofs; an exhaustive search over runs, reversals and disposals. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj
9 lines
216 B
Lean4
9 lines
216 B
Lean4
import Wanderbooks.Basic
|
|
import Wanderbooks.Entry
|
|
import Wanderbooks.Statements
|
|
import Wanderbooks.Closing
|
|
import Wanderbooks.Ledger
|
|
import Wanderbooks.Apportion
|
|
import Wanderbooks.Parties
|
|
import Wanderbooks.Prorate
|