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

fix: incorrect inherit_doc (#11704)

Browse source 
This PR fixes an incorrect `inherit_doc` in `Init.System.IO`.
This commit is contained in:
Markus Himmel 2025-12-16 18:30:01 +01:00 • committed by GitHub
parent b7f1cf9ba7
commit 7ba21c4d1b
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/Init/System/IO.lean
View file

@ -196,7 +196,7 @@ causing the side effect to occur at initialization time, even if it would otherw
@[inline] unsafe def unsafeEIO (fn : EIO ε α) : Except ε α :=
unsafeBaseIO fn.toBaseIO
@[inline, inherit_doc EIO] unsafe def unsafeIO (fn : IO α) : Except IO.Error α :=
@[inline, inherit_doc unsafeEIO] unsafe def unsafeIO (fn : IO α) : Except IO.Error α :=
unsafeEIO fn