From fb83af59484ca1ffee4ede761e58750837ce2c21 Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Thu, 29 Oct 2026 05:02:12 -0600 Subject: [PATCH] verify(lean): one docstring on Books after the S5 and S7 merges The S7 merge kept both branches' doc comments for the Books structure, S5's (which names the sends) stranded above an unrelated theorem and S7's on the structure; Lean refused the stray one. S5's text stays, on the structure it describes. Kani's 52 harnesses verified in the same run; only Lean's build stopped. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp --- verify/lean/Wanderbooks/Documents.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/verify/lean/Wanderbooks/Documents.lean b/verify/lean/Wanderbooks/Documents.lean index d8198c9..c4808e9 100644 --- a/verify/lean/Wanderbooks/Documents.lean +++ b/verify/lean/Wanderbooks/Documents.lean @@ -177,9 +177,6 @@ control guard requires of every entry a command posts. -/ def Tagged (control : List Nat) (ls : List TLine) : Prop := ∀ l ∈ ls, l.line.account ∈ control → l.doc ≠ none -/-- The books: the control accounts (the receivables and payables roles), -every posted line in order, and the sends recorded (each on its invoice; -plan P4b S5). -/ /-- A tagged list moves nothing that is unattached on a control account: no line it adds on one carries no document. -/ theorem unattached_zero_of_tagged {control : List Nat} {e : List TLine} (h : Tagged control e) @@ -202,8 +199,9 @@ def writeOffLines (control expense d D : Nat) (amount : Int) : List TLine := [ { line := { account := control, side := .credit, amount := amount }, date := D, doc := some d }, { line := { account := expense, side := .debit, amount := amount }, date := D, doc := none } ] -/-- The books: the control accounts (the receivables and payables roles) -and every posted line, in order. -/ +/-- The books: the control accounts (the receivables and payables roles), +every posted line in order, and the sends recorded (each on its invoice; +plan P4b S5). -/ structure Books where control : List Nat lines : List TLine