Documentation

Lean.Elab.Quotation.Precheck

source
structure Lean.Elab.Term.Quotation.Precheck.Context :
Type
Instances For
    source
    @[inline, reducible]
    abbrev Lean.Elab.Term.Quotation.PrecheckM (α : Type) :
    Type
    Instances For
      source
      @[inline, reducible]
      abbrev Lean.Elab.Term.Quotation.Precheck :
      Type
      Instances For
        source
        def Lean.Elab.Term.Quotation.withNewLocal {α : Type} (l : Lake.Name) (x : Lean.Elab.Term.Quotation.PrecheckM α) :
        Lean.Elab.Term.Quotation.PrecheckM α
        Instances For
          source
          def Lean.Elab.Term.Quotation.withNewLocals {α : Type} (ls : Array Lake.Name) (x : Lean.Elab.Term.Quotation.PrecheckM α) :
          Lean.Elab.Term.Quotation.PrecheckM α
          Instances For
            source
            opaque Lean.Elab.Term.Quotation.quotPrecheck :
            Lean.Option Bool
            source
            opaque Lean.Elab.Term.Quotation.quotPrecheck.allowSectionVars :
            Lean.Option Bool
            source
            unsafe def Lean.Elab.Term.Quotation.mkPrecheckAttribute :
            IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.Quotation.Precheck)
            Instances For
              source
              opaque Lean.Elab.Term.Quotation.precheckAttribute :
              Lean.KeyedDeclsAttribute Lean.Elab.Term.Quotation.Precheck
              source
              partial def Lean.Elab.Term.Quotation.precheck :
              Lean.Elab.Term.Quotation.Precheck
              source
              partial def Lean.Elab.Term.Quotation.precheck.hasQuotedIdent :
              Lean.Syntax → Bool
              source
              def Lean.Elab.Term.Quotation.runPrecheck (stx : Lean.Syntax) :
              Lean.Elab.TermElabM Unit
              Instances For
                source
                def Lean.Elab.Term.Quotation.precheckIdent :
                Lean.Elab.Term.Quotation.Precheck
                Instances For
                  source
                  def Lean.Elab.Term.Quotation.precheckApp :
                  Lean.Elab.Term.Quotation.Precheck
                  Instances For
                    source
                    def Lean.Elab.Term.Quotation.precheckTypeAscription :
                    Lean.Elab.Term.Quotation.Precheck
                    Instances For
                      source
                      def Lean.Elab.Term.Quotation.precheckExplicit :
                      Lean.Elab.Term.Quotation.Precheck
                      Instances For
                        source
                        def Lean.Elab.Term.Quotation.precheckChoice :
                        Lean.Elab.Term.Quotation.Precheck
                        Instances For
                          source
                          def Lean.Elab.Term.Quotation.elabPrecheckedQuot :
                          Lean.Elab.Term.TermElab
                          Instances For