Documentation

Lean.Elab.BuiltinNotation

source
def Lean.Elab.Term.elabCoe :
TermElab
Equations
    Instances For
      source
      def Lean.Elab.Term.elabCoeFunNotation :
      TermElab
      Equations
        Instances For
          source
          def Lean.Elab.Term.elabCoeSortNotation :
          TermElab
          Equations
            Instances For
              source
              def Lean.Elab.Term.elabAnonymousCtor :
              TermElab
              Equations
                Instances For
                  source
                  def Lean.Elab.Term.elabBorrowed :
                  TermElab
                  Equations
                    Instances For
                      source
                      def Lean.Elab.Term.expandShow :
                      Macro
                      Equations
                        Instances For
                          source
                          def Lean.Elab.Term.elabShow :
                          TermElab
                          Equations
                            Instances For
                              source
                              def Lean.Elab.Term.expandSuffices :
                              Macro
                              Equations
                                Instances For
                                  source
                                  def Lean.Elab.Term.elabLeadingParserMacro :
                                  TermElab
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Elab.Term.elabTrailingParserMacro :
                                      TermElab
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Elab.Term.elabPanic :
                                          TermElab
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Elab.Term.expandUnreachable :
                                              Macro
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Elab.Term.expandAssert :
                                                  Macro
                                                  Equations
                                                    Instances For
                                                      source
                                                      opaque Lean.Elab.Term.debugAssertions :
                                                      Lean.Option Bool
                                                      source
                                                      def Lean.Elab.Term.elabDebugAssert :
                                                      TermElab
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Elab.Term.expandDbgTrace :
                                                          Macro
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lean.Elab.Term.elabSorry :
                                                              TermElab
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.Elab.Term.mkPairs (elems : Array Term) :
                                                                  MacroM Term

                                                                  Return syntax Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))

                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lean.Elab.Term.mkPPairs (elems : Array Term) :
                                                                      MacroM Term

                                                                      Return syntax PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))

                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lean.Elab.Term.mkMPairs (elems : Array Term) :
                                                                          MacroM Term

                                                                          Return syntax MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))

                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Lean.Elab.Term.isCDotBinderKind (k : SyntaxNodeKind) :
                                                                              Bool
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.Elab.Term.isCDotForInfo (s : Syntax) (hygieneInfo? : Option Name) :
                                                                                  Bool

                                                                                  Returns whether or not this cdot is for the given HygieneInfo name; if no hygiene info is given, then matches any cdot, no matter its hygieneInfo.

                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      partial def Lean.Elab.Term.hasCDot :
                                                                                      Syntax → Option Name → Bool

                                                                                      Returns true if the given expression contains a cdot for the given HygieneInfo name. If no HygieneInfo name is given, then returns true if there is any cdot. The search is delimited by cdot binders (any syntax satisfying isCDotBinderKind).

                                                                                      source
                                                                                      def Lean.Elab.Term.expandCDot? (stx : Term) (hygieneInfo? : Option Name) :
                                                                                      MacroM (Option Term)

                                                                                      If the term contains any cdots that match the given HygieneInfo name (see isCDotForInfo), then returns some with the expanded syntax, otherwise returns none.

                                                                                      Examples:

                                                                                      • · + 1 => fun x => x + 1
                                                                                      • f · · b => fun x1 x2 => f x1 x2 b
                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.Elab.Term.elabCDotFunctionAlias? (stx : Term) :
                                                                                          TermElabM (Option Expr)

                                                                                          Helper method for elaborating terms such as (.+.) where a constant name is expected. This method is usually used to implement tactics that take function names as arguments (e.g., simp).

                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.Elab.Term.expandParen :
                                                                                              Macro
                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def Lean.Elab.Term.expandTuple :
                                                                                                  Macro
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Lean.Elab.Term.expandTypeAscription :
                                                                                                      Macro
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Lean.Elab.Term.elabTypeAscription :
                                                                                                          TermElab
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lean.Elab.Term.elabSubst :
                                                                                                              TermElab
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lean.Elab.Term.elabStateRefT :
                                                                                                                  TermElab
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Lean.Elab.Term.elabNoindex :
                                                                                                                      TermElab
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Lean.Elab.Term.elabUnsafe :
                                                                                                                          TermElab
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Lean.Elab.Term.elabRunElab :
                                                                                                                              TermElab

                                                                                                                              Elaborator for by_elab.

                                                                                                                              Equations
                                                                                                                                Instances For