• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Removable-runes
      • Fgl
      • 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
          • Rp-utilities
            • Defthmrp
            • Show-rules
            • Def-rw-opener-error
            • Valid-sc
            • Set-rp-backchain-limit
            • Fetch-new-theory
            • Ex-from-rp
            • Rp-other-utilities
            • Rp-equal
            • Preserve-current-theory
            • Set-rw-step-limit
            • Rp-termp
              • Include-fnc
              • Set-rp-backchain-limit-throws-error
              • Defwarrant-rp
              • Create-case-match-macro
            • 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-utilities

    Rp-termp

    Similarly to pseudo-termp, defines the syntax for terms.

    Signature
    (rp-termp term) → *