Documentation

Lean.Elab.BuiltinTerm

source
def Lean.Elab.Term.elabProp :
TermElab
Equations
    Instances For
      source
      def Lean.Elab.Term.elabSort :
      TermElab
      Equations
        Instances For
          source
          def Lean.Elab.Term.elabTypeStx :
          TermElab
          Equations
            Instances For

              the method resolveName adds a completion point for it using the given expected type. Thus, we propagate the expected type if stx[0] is an identifier. It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case. Recall that if the name resolution fails a synthetic sorry is returned.

              source
              def Lean.Elab.Term.elabPipeCompletion :
              TermElab
              Equations
                Instances For
                  source
                  def Lean.Elab.Term.elabCompletion :
                  TermElab
                  Equations
                    Instances For
                      source
                      def Lean.Elab.Term.elabHole :
                      TermElab
                      Equations
                        Instances For
                          source
                          def Lean.Elab.Term.elabSyntheticHole :
                          TermElab
                          Equations
                            Instances For
                              source
                              def Lean.Elab.Term.elabOmission :
                              TermElab
                              Equations
                                Instances For
                                  source
                                  def Lean.Elab.Term.elabLetMVar :
                                  TermElab
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Elab.Term.elabWaitIfTypeMVar :
                                      TermElab
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Elab.Term.elabWaitIfTypeContainsMVar :
                                          TermElab
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Elab.Term.elabWaitIfContainsMVar :
                                              TermElab
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Elab.Term.elabByTactic :
                                                  TermElab
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Elab.Term.elabNoImplicitLambda :
                                                      TermElab
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Elab.Term.elabBadCDot :
                                                          TermElab
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lean.Elab.Term.elabStrLit :
                                                              TermElab
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.Elab.Term.elabNumLit :
                                                                  TermElab
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lean.Elab.Term.elabRawNatLit :
                                                                      TermElab
                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lean.Elab.Term.elabScientificLit :
                                                                          TermElab
                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Lean.Elab.Term.elabCharLit :
                                                                              TermElab
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.Elab.Term.elabQuotedName :
                                                                                  TermElab
                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.Elab.Term.elabDoubleQuotedName :
                                                                                      TermElab
                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.Elab.Term.elabDeclName :
                                                                                          TermElab
                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.Elab.Term.elabWithDeclName :
                                                                                              TermElab
                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def Lean.Elab.Term.elabTypeOf :
                                                                                                  TermElab
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Lean.Elab.Term.elabEnsureTypeOf :
                                                                                                      TermElab
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Lean.Elab.Term.elabEnsureExpectedType :
                                                                                                          TermElab
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lean.Elab.Term.elabValueOf :
                                                                                                              TermElab
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lean.Elab.Term.elabClear :
                                                                                                                  TermElab
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Lean.Elab.Term.elabOpen :
                                                                                                                      TermElab
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Lean.Elab.Term.elabSetOption :
                                                                                                                          TermElab
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Lean.Elab.Term.elabWithAnnotateTerm :
                                                                                                                              TermElab
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  def Lean.Elab.Term.elabIncludeStr :
                                                                                                                                  TermElab
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      def Lean.Elab.Term.elabNamedPatternErr :
                                                                                                                                      TermElab
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          def Lean.Elab.Term.elabPrivateDecl :
                                                                                                                                          TermElab
                                                                                                                                          Equations
                                                                                                                                            Instances For