Update link to FFI docs to the reference guide

It's a separate matter that these docs are duplicated at the moment. Thanks @jcreedcmu for noting the duplication and @david-christiansen for canonical link

README.md

@@ -2,19 +2,19 @@ This is the repository for **Lean 4**.
 
 # About
 
-- [Quickstart](https://lean-lang.org/documentation/setup/)
+- [Quickstart](https://lean-lang.org/install/)
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Documentation Overview](https://lean-lang.org/documentation/)
+- [Documentation Overview](https://lean-lang.org/learn/)
 - [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/lean4/doc/examples.html)
+- [Examples](https://lean-lang.org/examples/)
 - [External Contribution Guidelines](CONTRIBUTING.md)
 
 # Installation
 
-See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
+See [Install Lean](https://lean-lang.org/install/).
 
 # Contributing
 

src/Lean/Expr.lean

@@ -70,7 +70,7 @@ def bar ⦃x : Nat⦄ : Nat := x
 #check bar -- bar : ⦃x : Nat⦄ → Nat
 ```
 
-See also [the Lean manual](https://lean-lang.org/lean4/doc/expressions.html#implicit-arguments).
+See also [the Lean Language Reference](https://lean-lang.org/doc/reference/latest/Terms/Functions/#implicit-functions).
 -/
 inductive BinderInfo where
   /-- Default binder annotation, e.g. `(x : α)` -/

src/Lean/Parser/Term.lean

@@ -568,7 +568,7 @@ Being borrowed only affects the ABI and runtime behavior of the function when co
 
 When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.
 
-Please see https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing for a complete description.
+Please see https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-borrowing for a complete description.
 -/
 @[builtin_term_parser] def borrowed   := leading_parser
   "@& " >> termParser leadPrec

src/Lean/Widget/Types.lean

@@ -44,7 +44,7 @@ or use a value of `javascript` identical to that of another definition
 annotated with `@[widget_module]`.
 This makes it possible for the infoview to load the module.
 
-See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+See the [manual entry](https://lean-lang.org/examples/1900-1-1-widgets/)
 for more information on how to use the widgets system. -/
 structure Module where
   /-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)