Documentation

DocGen4.Process.DocInfo

source
def DocGen4.Process.DocInfo.getDeclarationRange :
DocInfo → Lean.DeclarationRange
Equations
Instances For
    source
    def DocGen4.Process.DocInfo.getName :
    DocInfo → Lean.Name
    Equations
    Instances For
      source
      def DocGen4.Process.DocInfo.getKind :
      DocInfo → String
      Equations
      Instances For
        source
        def DocGen4.Process.DocInfo.getType :
        DocInfo → RenderedCode
        Equations
        Instances For
          source
          def DocGen4.Process.DocInfo.getArgs :
          DocInfo → Array Arg
          Equations
          Instances For
            source
            def DocGen4.Process.DocInfo.getSorried :
            DocInfo → Bool
            Equations
            Instances For
              source
              def DocGen4.Process.DocInfo.getAttrs :
              DocInfo → Array String
              Equations
              Instances For
                source
                def DocGen4.Process.DocInfo.getDocString :
                DocInfo → Option (String ⊕ Lean.VersoDocString)
                Equations
                Instances For
                  source
                  def DocGen4.Process.DocInfo.getMarkdownDocString (i : DocInfo) :
                  Option String
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def DocGen4.Process.DocInfo.shouldRender :
                    DocInfo → Bool
                    Equations
                    Instances For
                      source
                      def DocGen4.Process.DocInfo.isCtorInfo :
                      DocInfo → Bool
                      Equations
                      Instances For
                        source
                        def DocGen4.Process.DocInfo.isProjFn (declName : Lean.Name) :
                        Lean.MetaM Bool

                        Returns true if declName is a field projection or a parent projection for a structure.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def DocGen4.Process.DocInfo.isBlackListed (declName : Lean.Name) :
                          Lean.MetaM Bool
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def DocGen4.Process.DocInfo.ofConstant :
                            Lean.Name × Lean.ConstantInfo → AnalyzeM (Option DocInfo)
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def DocGen4.Process.DocInfo.getKindDescription :
                              DocInfo → String
                              Equations
                              Instances For