From 10e7d79389c8576a705a528adff53c81d522fdf4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Mar 2025 17:24:17 +0100
Subject: [PATCH] clarify notation

---
 theories/tree_borrows/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index c984d8a1..3ba9ba33 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -149,7 +149,7 @@ This program logic can prove refinements, and uses several separation logic reso
 You can see the separation logic in action in the examples shown above.
 Here, we explain the resources that you will encounter when stepping through the proof.
 
-The `$$` resource associates a "tag" with a "tag kind." Remember that each tag corresponds to a specific node in the borrow tree.
+The `t $$ tk` resource associates a "tag" `t` with a "tag kind" `tk`. Remember that each tag corresponds to a specific node in the borrow tree.
 The tag kind is a very coarse over-approximation of the shape of the tree from that specific node.
 
 The simplest kind is `tk_local`, which says that the tree here is a singleton, and this tag is the only tag in the tree.
-- 
GitLab