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

doc: fix link to initialization section in ffi section

Browse source 
The current link goes to doc/dev#init, where there is nothing
about initialization. This PR fixes the link so that it points
to the initialization section lower down on the ffi page.
This commit is contained in:
David Renshaw 2022-10-07 11:17:17 -04:00 • committed by Sebastian Ullrich
parent 4fa1a496b3
commit 5c7cf76575
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/dev/ffi.md
View file

@ -21,7 +21,7 @@ If `n` is 0, the corresponding C declaration is
extern s sym;
```
where `s` is the C translation of `β` as specified in the next section.
In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](.#init).
In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](#initialization).
If `n` is greater than 0, the corresponding C declaration is
```c