max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Fix doc bug in Resolve.lean (#8411)

Browse source 
This PR fixes a doc bug in the Resolve.lean; in reverse order, B comes
before A
This commit is contained in:
Li Xuanji 2025-05-20 13:16:18 -04:00 • committed by GitHub
parent 8753239226
commit a9a069a0ef
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lake/Lake/Load/Resolve.lean
View file

@ -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.