Partial Functions in ACL2

---

Panagiotis Manolios and J Strother Moore.
ACL2 Workshop 2000.

Abstract

We describe a macro for introducing ``partial functions'' into ACL2, i.e., functions not defined everywhere. The function ``definitions'' are actually admitted via the encapsulation principle. We discuss the basic issues surrounding partial functions in ACL2 and illustrate theorems that can be proved about such functions.

Gzipped Postscript (55K)