elab 使用例: section の中でしか使用できない名前を定義する

[Seasawher]

open Lean Elab Command

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

private section
  def foo := "hello!!"

  -- セクションの中なら当然アクセスできる
  #check foo
end private section

-- `foo` にアクセスできない
#check_failure foo

[Seasawher]

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/private.20section/near/418114975