From e0fcaf5e7ddab2fcab51be8c403446d84a8a0d45 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 11 Aug 2025 08:43:30 +0200 Subject: [PATCH] chore: Naming in `Invariant.withEarlyReturn` (#9835) Just a small renaming leftover. --- src/Std/Do/Triple/SpecLemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index 3113900375..71e8afaf30 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -342,12 +342,12 @@ another iteration of the loop body. abbrev Invariant.withEarlyReturn (onContinue : List.Zipper xs → β → Assertion ps) (onReturn : γ → β → Assertion ps) - (onFail : ExceptConds ps := ExceptConds.false) : + (onExcept : ExceptConds ps := ExceptConds.false) : Invariant xs (MProd (Option γ) β) ps := ⟨fun ⟨xs, x, b⟩ => spred( (⌜x = none⌝ ∧ onContinue xs b) ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suff = []⌝ ∧ onReturn r b)), - onFail⟩ + onExcept⟩ @[spec] theorem Spec.forIn'_list {α β : Type u}