• 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
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
      • Use-termhint
        • Function-termhint
        • Termhint-seq
        • Process-termhint
        • Hq
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Use-termhint

Process-termhint

Processes termhint objects into regular hint objects.

Essentially this function is an interpreter for terms containing calls of cons and binary-append, as well as quoted and pseudo-quoted objects (see below), which are both treated the same. If any other functions or any variable atoms are present, it produces an error.

This capability is intended to be enough to process backtick expressions where all the commas are accompanied by hq (or other pseudoquote) calls; e.g.:

 (let ((my-a (foo bar baz)))
   (process-termhint `'(:use my-theorem (a ,(hq my-a)))))
=>
 (:USE MY-THEOREM (A (FOO BAR BAZ)))

Process-termhint is always called with quote and hq present in quotesyms, but there may also be others according to the termhint quotesyms list, which is stored in a table:

(table termhint 'quotesyms)   ;; show the list of quotesyms
(cdr (assoc 'quotesyms (table-alist termhint world))) ;; access the list of quotesyms
(termhint-add-quotesym my-quotesym) ;; add a new quotesym