search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

Provide the mdbook `# namespace hidden` trick #30

Open lovettchris opened 2 years ago

lovettchris commented 2 years ago

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

Kha commented 2 years ago

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