P2M helper commands (scope and alias plumbing)

Definition: P2M_Util (217e943d-2223-5c63-9415-3c10daa2cd91), by Claude, 2026-09-05.

Helper commands used by the FLT proof files to restore namespace/scope context after the project was split into one-declaration modules. The opening commands elaborate native open commands; exports create aliases. These helpers add no mathematical declarations or axioms.

<!-- Generated by add_prove2me_provenance.py -->

def p2mOpenCore (s : String) : Lean.Elab.Command.CommandElabM Unit

Opens the space-separated namespaces in s and activates their scoped extensions. An entry N~x~y hides x and y from ordinary name lookup through this opening of N. Shared implementation of p2m_open and its command-local form.

Equations

• One or more equations did not get rendered due to their size.

def commandP2m_open_ : Lean.ParserDescr

p2m_open "N M" opens the listed namespaces and activates their scoped extensions. Use N~x~y to hide names x and y when opening N. Empty entries are ignored. The openings last for the current scope; use p2m_open "N M" in cmd for one command.

Equations

• commandP2m_open_ = Lean.ParserDescr.node `commandP2m_open_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "p2m_open ") (Lean.ParserDescr.const `str))

def commandP2m_open_scoped_ : Lean.ParserDescr

p2m_open_scoped "N M" activates the listed namespaces' scoped extensions without opening ordinary names. Empty entries are ignored, and any ~... suffix is discarded. Use p2m_open_scoped "N M" in cmd to restrict activation to one command.

Equations

• commandP2m_open_scoped_ = Lean.ParserDescr.node `commandP2m_open_scoped_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "p2m_open_scoped ") (Lean.ParserDescr.const `str))

def p2mOpenIn : Lean.ParserDescr

p2m_open "N M" in cmd opens namespaces and activates their scoped extensions only within cmd, by wrapping the opening and command in a temporary section. Supports the same N~x~y hiding syntax as p2m_open.

Equations

• One or more equations did not get rendered due to their size.

def commandP2m_export__ : Lean.ParserDescr

p2m_export "N" "a b" aliases N.a and N.b as a and b in the current namespace. For each target, tries the ordinary declaration name, then its private name in the current module. Silently skips missing targets and empty entries. Creates aliases, not new proofs.

Equations

• One or more equations did not get rendered due to their size.

def commandP2m_open_scoped_In_ : Lean.ParserDescr

p2m_open_scoped "N M" in cmd activates scoped extensions only within cmd, using a temporary section. Does not open ordinary names.

Equations

• One or more equations did not get rendered due to their size.