Hiding certain Lean imports at the beginging of a chapter - Githubissues

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

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

Open lovettchris opened 2 years ago

lovettchris commented 2 years ago

Description

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

Detailed behaviour

Testscenarios

References