• Top
  • Documentation
  • Books
    • Cert.pl
    • Community-books
    • Project-dir-alist
    • Bookdata
    • Uncertified-books
    • Book-hash
    • Sysfile
    • Show-books
    • Best-practices
    • Books-reference
    • Where-do-i-place-my-book
    • Books-tour
      • Include-book
      • Certify-book
      • Certificate
      • Portcullis
      • Book-name
      • Book-example
      • Book-contents
      • Keep
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Books

Books-tour

The guided tour of concepts related to ACL2 books.

The tour begins with book-example.

Subtopics

Include-book

Load the events in a file

Certify-book

How to produce a certificate for a book

Certificate

A file specifying validity of a given book

Portcullis

The gate guarding the entrance to a certified book

Book-name

Conventions associated with book-names

Book-example

How to create, certify, and use a simple book

Book-contents

Restrictions on the forms inside books

Keep

How we know if include-book read the correct files