scoped[NS] syntax

This is a replacement for the localized command in mathlib. It is similar to scoped, but it scopes the syntax in the specified namespace instead of the current namespace.

def Mathlib.Tactic.scopedNS : Lean.ParserDescr

scoped[NS] is similar to the scoped modifier on attributes and notations, but it scopes the syntax in the specified namespace instead of the current namespace.

scoped[Matrix] postfix:1024 "ᵀ" => Matrix.transpose
-- declares `ᵀ` as a notation for matrix transposition
-- which is only accessible if you `open Matrix` or `open scoped Matrix`.

namespace Nat

scoped[Nat.Count] attribute [instance] CountSet.fintype
-- make the definition Nat.CountSet.fintype an instance,
-- but only if `Nat.Count` is open

Equations

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