chore: Naming in Invariant.withEarlyReturn (#9835)
Just a small renaming leftover.
This commit is contained in:
parent
1b78d8f0a3
commit
e0fcaf5e7d
1 changed files with 2 additions and 2 deletions
|
|
@ -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}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue