• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Terminal
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
        • Entities
        • Defxdoc+
        • Save-rendered
        • Add-resource-directory
        • Testing
        • Order-subtopics
        • Save-rendered-event
        • Archive-matching-topics
        • Archive-xdoc
        • Xdoc-extend
        • Set-default-parents
        • Missing-parents
          • Interp-st-stack-backtrace-top
          • Interp-st-fn-annotation
          • Interp-st-stack-full-backtrace
          • Missing-parents-test
        • Defpointer
        • Defxdoc-raw
        • Xdoc-tests
        • Xdoc-prepend
        • Defsection-progn
        • Gen-xdoc-for-file
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
      • Pointers
      • Doc
      • Documentation-copyright
      • Course-materials
      • Publications
      • Args
      • ACL2-doc-summary
      • Finding-documentation
      • Broken-link
      • Doc-terminal-test-2
      • Doc-terminal-test-1
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Xdoc

Missing-parents

Placeholder for documentation topics that lack :parents.

If a defxdoc form ends up having no parents, it ends up being put here. See also undocumented.

Historic note. We used to put these topics directly underneath top instead. But we found that during development, this sometimes led to a strange-looking hierarchy where ``random'' topics were presented as top-level topics just because they were new or being moved around or because set-default-parents forms weren't quite in the right places. To avoid this, we now move these topics to missing-parents and print notes about them when a manual is saved with save.

Subtopics

Interp-st-stack-backtrace-top
Produce a backtrace frame for the top FGL rewriter stack frame that matches any of a list of rule specifications
Interp-st-fn-annotation
Finds the annotation, if any, of the innermost nesting of fn on the stack.
Interp-st-stack-full-backtrace
Produce a full backtrace for the FGL rewriter stack, containing all top-level bindings of all rules
Missing-parents-test
A topic with no :parents.