Documentation

Lean.Elab.Notation

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

      Convert notation command lhs item into a syntax command item

      Equations
        Instances For

          Convert notation command lhs item into a pattern element

          Equations
            Instances For
              Equations
                Instances For
                  def Lean.Elab.Command.mkUnexpander (attrKind : TSyntax `Lean.Parser.Term.attrKind) (pat qrhs : Term) :

                  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
                    Instances For