Documentation

Lean.Elab.BuiltinNotation

source
def Lean.Elab.Term.elabCoe :
TermElab
Instances For
    source
    def Lean.Elab.Term.elabCoeFunNotation :
    TermElab
    Instances For
      source
      def Lean.Elab.Term.elabCoeSortNotation :
      TermElab
      Instances For
        source
        def Lean.Elab.Term.elabAnonymousCtor :
        TermElab
        Instances For
          source
          def Lean.Elab.Term.elabBorrowed :
          TermElab
          Instances For
            source
            def Lean.Elab.Term.expandShow :
            Macro
            Instances For
              source
              def Lean.Elab.Term.elabShow :
              TermElab
              Instances For
                source
                def Lean.Elab.Term.expandSuffices :
                Macro
                Instances For
                  source
                  def Lean.Elab.Term.elabLeadingParserMacro :
                  TermElab
                  Instances For
                    source
                    def Lean.Elab.Term.elabTrailingParserMacro :
                    TermElab
                    Instances For
                      source
                      def Lean.Elab.Term.elabPanic :
                      TermElab
                      Instances For
                        source
                        def Lean.Elab.Term.expandUnreachable :
                        Macro
                        Instances For
                          source
                          def Lean.Elab.Term.expandAssert :
                          Macro
                          Instances For
                            source
                            opaque Lean.Elab.Term.debugAssertions :
                            Lean.Option Bool
                            source
                            def Lean.Elab.Term.elabDebugAssert :
                            TermElab
                            Instances For
                              source
                              def Lean.Elab.Term.expandDbgTrace :
                              Macro
                              Instances For
                                source
                                def Lean.Elab.Term.elabSorry :
                                TermElab
                                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])))

                                  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])))

                                    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])))

                                      Instances For
                                        source
                                        def Lean.Elab.Term.isCDotBinderKind (k : SyntaxNodeKind) :
                                        Bool
                                        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.

                                          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
                                            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).

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

                                                                Elaborator for by_elab.

                                                                Instances For