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] infixl:72 " ⬝ᵥ " => Matrix.dotProduct
-- declares `*` as a notation for vector dot productss
-- 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.