termSpec(_) — Mathlib

Lean4
/-- The spectrum of an unbundled ring as a scheme.
WARNING: This is potentially confusing as `Spec (R)` and `Spec(R)` have different meanings.
Hence we avoid using it in mathlib but leave it as a scoped instance for downstream projects.

WARNING: If `R` is already an element of `CommRingCat`, you should use `Spec R` instead of
`Spec(R)`, which is secretly `Spec(↑R)`. -/
@[scoped term_parser 1000]
public meta def «termSpec(_)» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `SpecOfNotation.«termSpec(_)» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "Spec(") (ParserDescr.cat✝ `term 0)) (ParserDescr.symbol✝ ")"))
Похожие утверждения