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.

ink

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] infixl:75 " ⬝ " => Matrix.mul
-- declares `⬝` as a notation for matrix multiplication
-- 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
⬝ " => Matrix.mul
-- declares `⬝` as a notation for matrix multiplication
-- 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
⬝` as a notation for matrix multiplication
-- 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.