## Description Is there a way to hide this lean import at the top of this chapter on the [State monad](https://github.com/leanprover/lean4/pull/1505/files#diff-4ebb38f5aa40768ff6ea4b8544a47e3fda4927271dc1fe10b1d9f73432e18a43)?  ## Detailed behaviour <!--- Describe the feature here in detail. Point out important goals for the completion of the feature. Also make sure to list important edge cases that must be taken into consideration during implementation. --> ## Testscenarios <!--- Describe one or more test scenarios for the new feature. Preferably as a list of sequential tasks + tests. --> ## References <!--- List of references for the feature request. -->
Description
Is there a way to hide this lean import at the top of this chapter on the State monad?
Detailed behaviour
Testscenarios
References