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.expandHave :
                              Macro
                              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
                                                                          partial def Lean.Elab.Term.mkPairs.loop (elems : Array Term) (i : Nat) (acc : Term) :
                                                                          MacroM Term
                                                                          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
                                                                              partial def Lean.Elab.Term.mkPPairs.loop (elems : Array Term) (i : Nat) (acc : Term) :
                                                                              MacroM Term
                                                                              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
                                                                                  partial def Lean.Elab.Term.mkMPairs.loop (elems : Array Term) (i : Nat) (acc : Term) :
                                                                                  MacroM Term
                                                                                  source
                                                                                  partial def Lean.Elab.Term.hasCDot :
                                                                                  Syntax → Bool
                                                                                  source
                                                                                  def Lean.Elab.Term.expandCDot? (stx : Term) :
                                                                                  MacroM (Option Term)

                                                                                  Return some if succeeded expanding · notation occurring in the given syntax. Otherwise, return none. Examples:

                                                                                  • · + 1 => fun x => x + 1
                                                                                  • f · · b => fun x1 x2 => f x1 x2 b
                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      partial def Lean.Elab.Term.expandCDot?.go :
                                                                                      Syntax → StateT (Array Ident) MacroM Syntax

                                                                                      Auxiliary function for expanding the · notation. The extra state Array Syntax contains the new binder names. If stx is a ·, we create a fresh identifier, store it in the extra state, and return it. Otherwise, we just return stx.

                                                                                      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.elabCDotFunctionAlias?.expandCDotArg? (stx : Term) :
                                                                                          MacroM (Option Term)
                                                                                          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
                                                                                                                                  source
                                                                                                                                  def Lean.Elab.Term.elabHaveI :
                                                                                                                                  TermElab
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      def Lean.Elab.Term.elabLetI :
                                                                                                                                      TermElab
                                                                                                                                      Equations
                                                                                                                                        Instances For