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.
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.