From a3c294e10fbae8114c129d8069a56b10cd1fe145 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <johannesmatthias.hostert@inf.ethz.ch>
Date: Fri, 15 Nov 2024 07:49:26 +0000
Subject: [PATCH] Apply suggestion

---
 theories/tree_borrows/read_read_reorder/equivalence_def.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/tree_borrows/read_read_reorder/equivalence_def.v b/theories/tree_borrows/read_read_reorder/equivalence_def.v
index 8a3b266d..2892d463 100644
--- a/theories/tree_borrows/read_read_reorder/equivalence_def.v
+++ b/theories/tree_borrows/read_read_reorder/equivalence_def.v
@@ -24,7 +24,8 @@ Inductive no_termination_within P : expr → state → nat → Prop :=
     (∀ e' σ', prim_step P e σ e' σ' nil → no_termination_within P e' σ' n) →
     no_termination_within P e σ (S n).
 
-(* Two programs are eventually equal if they both do not terminate with n steps,
+(* Two programs are eventually equal if there exists an n such that they
+   both do not terminate with n steps,
   and after n steps, they are equal. *)
 Definition eventually_equal P e1 e2 :=
   ∃ n, ∀ σ, state_wf σ →
-- 
GitLab