ACL2 Seminar, May 4, 2018

Speaker: Matt Kaufmann

Title: A Brief Introduction to Make-Event

Abstract:

The ACL2 utility, make-event, was first introduced in ACL2 Version 3.0, in June, 2006. A quick calculation suggests more than 1,800 calls of make-event in the community books. Nevertheless, this utility may remain mysterious to many ACL2 users.

This talk will consist of two parts. First I'll take people through the first part of the make-event documentation, providing ample opportunity to ask questions. Then, as time permits, I'll take people through a somewhat complex example, from community book make-event/search-generation.lisp.