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.