type-hyp

(in-package "SMT")

(include-book "std/util/bstar" :dir :system)

(include-book "std/testing/eval" :dir :system)

(include-book "clause-processors/join-thms" :dir :system)

(include-book "xdoc/top" :dir :system)

(include-book "std/util/define" :dir :system)

(include-book "centaur/fty/baselists" :dir :system)

(include-book "hint-interface")

(defsection smt-type-hyp
  :parents (verified)
  :short "The function type-hyp passes type related information onto the
  trusted clause processor."
  (define type-hyp
    ((blist boolean-listp) (tag symbolp))
    (b* ((blist (boolean-list-fix blist)) ((unless (consp blist)) t)
        ((cons first rest) blist))
      (and first (type-hyp rest tag))))
  (in-theory (disable (:d type-hyp)
      (:e type-hyp)
      (:t type-hyp))))