LeanInk icon indicating copy to clipboard operation
LeanInk copied to clipboard

Provide the mdbook `# namespace hidden` trick

Open lovettchris opened this issue 3 years ago • 1 comments

Description

Sometimes while writing you need to quote a piece of core std lib code, but you get errors already defined but you also don't want to have readable namespace hidden hacks around that code either.

So it would be nice to have what we had in mdbook with the hidden comment in the form # namespace hidden to work around this.

Detailed behaviour

Testscenarios

References

lovettchris avatar Aug 31 '22 00:08 lovettchris

This as well seems to be covered by https://github.com/cpitclaudel/alectryon#controlling-output (if we used Alectryon)

Kha avatar Aug 31 '22 08:08 Kha