This repository has been archived by the owner on Aug 24, 2024. It is now read-only.

Hiding certain Lean imports at the beginging of a chapter #25

Open

lovettchris opened this issue Aug 26, 2022 · 0 comments

Contributor

lovettchris commented Aug 26, 2022 •

edited

Loading

Description

Is there a way to hide this lean import at the top of this chapter on the State monad?

Detailed behaviour

Testscenarios

References

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.