term_~[_]_ — Mathlib

Lean4
/-- Notation for apply a relation `R : SetRel α β` to `a : α`, `b : β`,
scoped to the `SetRel` namespace.

Since `SetRel α β := Set (α × β)`, `a ~[R] b` is simply notation for `(a, b) ∈ R`, but this should
be considered an implementation detail. -/
@[scoped term_parser 1000]
public meta def «term_~[_]_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `SetRel.«term_~[_]_» 50 50
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ~[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 50))
Похожие утверждения