types

(in-package "BUILD2")

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

(defprod book-dep
  :short "A dependency on another book."
  ((path stringp
     "Path to the book (without .lisp extension).") (localp booleanp
      :default nil
      "Was this inside LOCAL?"))
  :tag :book-dep)

(deflist book-dep-list
  :elt-type book-dep
  :true-listp t)

(defprod certinfo
  :short "Information needed to certify a book."
  ((bookdeps book-dep-list-p
     :default nil
     "Books this book depends on (from include-book).") (srcdeps string-listp
      :default nil
      "Source files (.lisp, .acl2 files)."))
  :tag :certinfo)

(defalist certinfo-alist
  :key-type stringp
  :val-type certinfo
  :true-listp t)