From a9a069a0efb9cedce192ed50fcd9158e778232e9 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Tue, 20 May 2025 13:16:18 -0400
Subject: [PATCH] doc: Fix doc bug in Resolve.lean (#8411)

This PR fixes a doc bug in the Resolve.lean; in reverse order, B comes
before A
---
 src/lake/Lake/Load/Resolve.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean
index ebc4e70075..6cff35dfda 100644
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/src/lake/Lake/Load/Resolve.lean
@@ -318,7 +318,7 @@ R
 |- C
 ```
 
-Lake follows the order `R`, `C`, `A`, `B`, `Y`, `X`.
+Lake follows the order `R`, `C`, `B`, `A`, `Y`, `X`.
 
 The reason for this is two-fold:
 1. Like targets, later requires should shadow earlier definitions.