Documentation

Lean.Elab.Notation

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 ",")
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Convert notation command lhs item into a syntax command item

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Convert notation command lhs item into a pattern element

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.Elab.Command.mkUnexpander (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) (pat : Lean.Term) (qrhs : Lean.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
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For