private section

Stream: lean4

[Geoffrey Irving]

Is it possible to make a section that is entirely private (defs visible only in the current file)?

[Alex J. Best]

What do you mean by visible? Completely erased from the environment? Or simply only accessible via private names?

[Geoffrey Irving]

Concretely, if I declare something of the same name in another downstream file, it doesn't complain.

[Matthew Ballard]

If you want to write a macro for this, docs#elabSuppressCompilationDecl might be a good place to start.

[Markus Schmaus]

How about namespace?

[Max Nowak 🐉]

"Example sections" would be nice to have yeah.

[Alex J. Best]

Here's a really simple way to implement example section. I.e. a section in which you can do stuff but the whole state is completely reset after.

import Lean
open Lean Elab Command

elab "example section" ppLine cmd:command* ppLine "end example section": command => do
  let old ← get
  try
    for cmd in cmd do
      elabCommandTopLevel cmd
    throwAbortCommand
  finally
    set old


example section
namespace o
theorem toot : 1 = 1 := rfl
theorem toot2 : 1 = 1 := rfl

end example section
theorem toot : 1 = 1 := rfl

#print toot

#print o.toot2

[Alex J. Best]

Ok this version is too simplistic, resetting the env is not enough as it leaves namespaces open etc, but fully resetting the state means you dont see the error messages, so something inbetween would be better. Resetting the env using getEnv and setEnv in the above is better for now

[Jannis Limperg]

Try docs#Lean.withoutModifyingState and other functions from the same file. These intelligently revert the state, so traces and error messages stay intact (among other things).