• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Fgl
      • Removable-runes
      • Efficiency
      • Rewrite-bounds
      • Bash
      • Def-dag-measure
      • Bdd
      • Remove-hyps
      • Contextual-rewriting
      • Simp
      • Rewrite$-hyps
      • Bash-term-to-dnf
      • Use-trivial-ancestors-check
      • Minimal-runes
      • Clause-processor-tools
        • Rp-rewriter
          • Rp-ruleset
          • Defthmrp
          • Rp-rewriter/meta-rules
            • Add-meta-rule
            • Dont-rw
            • Attach-meta-fncs
            • Is-rp-clause-processor-up-to-date
            • Rp-utilities
            • Rp-rewriter-demo
            • Rp-rewriter/debugging
            • Rp-rewriter/applications
        • Fn-is-body
        • Without-subsumption
        • Rewrite-equiv-hint
        • Def-bounds
        • Rewrite$-context
        • Try-gl-concls
        • Hint-utils
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Rp-rewriter/meta-rules

    Is-rp-clause-processor-up-to-date

    Checks if all the added meta-rules are 'registered'

    After calling add-meta-rule or when different books with meta rules are included, users need to call attach-meta-fncs. This function checks if it is necessary.

    (is-rp-clause-processor-up-to-date world)