Documentation

Lean.Elab.Notation

source
def Lean.Elab.Command.addInheritDocDefault (rhs : Lean.Term) (attrs? : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) :
Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")
Instances For
    source
    def Lean.Elab.Command.expandNotationItemIntoSyntaxItem :
    Lean.TSyntax `Lean.Parser.Command.notationItem → Lean.MacroM (Lean.TSyntax `stx)

    Convert notation command lhs item into a syntax command item

    Instances For
      source
      def Lean.Elab.Command.expandNotationItemIntoPattern (stx : Lean.Syntax) :
      Lean.MacroM Lean.Syntax

      Convert notation command lhs item into a pattern element

      Instances For
        source
        def Lean.Elab.Command.removeParenthesesAux (parens body : Lean.Syntax) :
        Lean.Syntax
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          partial def Lean.Elab.Command.removeParentheses (stx : Lean.Syntax) :
          Lean.MacroM Lean.Syntax
          source
          def Lean.Elab.Command.hasDuplicateAntiquot (stxs : Array Lean.Syntax) :
          Bool
          Instances For
            source
            def Lean.Elab.Command.mkUnexpander (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) (pat qrhs : Lean.Term) :
            OptionT Lean.MacroM Lean.Syntax

            Try to derive an unexpander from a notation. The notation must be of the form notation ... => c body where c is a declaration in the current scope and body any syntax that contains each variable from the LHS at most once.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Elab.Command.expandNotation :
              Lean.Macro
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For