Documentation

Lean.Elab.Quotation.Precheck

source
structure Lean.Elab.Term.Quotation.Precheck.Context :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Elab.Term.Quotation.PrecheckM (α : Type) :
    Type
    Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Elab.Term.Quotation.Precheck :
        Type
        Equations
          Instances For
            source
            def Lean.Elab.Term.Quotation.withNewLocal {α : Type} (l : Name) (x : PrecheckM α) :
            PrecheckM α
            Equations
              Instances For
                source
                def Lean.Elab.Term.Quotation.withNewLocals {α : Type} (ls : Array Name) (x : PrecheckM α) :
                PrecheckM α
                Equations
                  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 (KeyedDeclsAttribute Precheck)
                    Equations
                      Instances For
                        source
                        opaque Lean.Elab.Term.Quotation.precheckAttribute :
                        KeyedDeclsAttribute Precheck
                        source
                        partial def Lean.Elab.Term.Quotation.precheck :
                        Precheck
                        source
                        partial def Lean.Elab.Term.Quotation.precheck.hasQuotedIdent :
                        Syntax → Bool
                        source
                        def Lean.Elab.Term.Quotation.runPrecheck (stx : Syntax) :
                        TermElabM Unit
                        Equations
                          Instances For
                            source
                            def Lean.Elab.Term.Quotation.precheckIdent :
                            Precheck
                            Equations
                              Instances For
                                source
                                def Lean.Elab.Term.Quotation.precheckApp :
                                Precheck
                                Equations
                                  Instances For
                                    source
                                    def Lean.Elab.Term.Quotation.precheckTypeAscription :
                                    Precheck
                                    Equations
                                      Instances For
                                        source
                                        def Lean.Elab.Term.Quotation.precheckExplicit :
                                        Precheck
                                        Equations
                                          Instances For
                                            source
                                            def Lean.Elab.Term.Quotation.precheckChoice :
                                            Precheck
                                            Equations
                                              Instances For
                                                source
                                                def Lean.Elab.Term.Quotation.elabPrecheckedQuot :
                                                TermElab
                                                Equations
                                                  Instances For
                                                    source
                                                    def Lean.Elab.Term.Quotation.precheckBinrel :
                                                    Precheck
                                                    Equations
                                                      Instances For
                                                        source
                                                        def Lean.Elab.Term.Quotation.precheckBinrelNoProp :
                                                        Precheck
                                                        Equations
                                                          Instances For
                                                            source
                                                            def Lean.Elab.Term.Quotation.precheckBinop :
                                                            Precheck
                                                            Equations
                                                              Instances For
                                                                source
                                                                def Lean.Elab.Term.Quotation.precheckBinopLazy :
                                                                Precheck
                                                                Equations
                                                                  Instances For
                                                                    source
                                                                    def Lean.Elab.Term.Quotation.precheckLeftact :
                                                                    Precheck
                                                                    Equations
                                                                      Instances For
                                                                        source
                                                                        def Lean.Elab.Term.Quotation.precheckRightact :
                                                                        Precheck
                                                                        Equations
                                                                          Instances For
                                                                            source
                                                                            def Lean.Elab.Term.Quotation.precheckUnop :
                                                                            Precheck
                                                                            Equations
                                                                              Instances For