From 0232e6a114d85b3644443d047dff0487f8b08b92 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 14 Mar 2025 17:37:51 +0100
Subject: [PATCH] add comment about nsteps

---
 theories/tree_borrows/read_read_reorder/equivalence_def.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/tree_borrows/read_read_reorder/equivalence_def.v b/theories/tree_borrows/read_read_reorder/equivalence_def.v
index 2892d463..4c3260d9 100644
--- a/theories/tree_borrows/read_read_reorder/equivalence_def.v
+++ b/theories/tree_borrows/read_read_reorder/equivalence_def.v
@@ -6,6 +6,7 @@ From iris.prelude Require Import options.
 
 (* [nsteps ... n] says that one can transition from one state to the other in exactly [n]
 primitive steps. *)
+(* This is similar to stdpp's [nsteps], except that this one computes more nicely for fixed [n]. *)
 Fixpoint nsteps P (e : expr) σ e'' σ'' n : Prop := match n with
   0 => e = e'' ∧ σ = σ''
 | S n => ∃ e' σ', prim_step P e σ e' σ' nil ∧ nsteps P e' σ' e'' σ'' n end.
-- 
GitLab