Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Partial Functions in ACL2

Panagiotis Manolios and J Strother Moore.
ACL2 Workshop 2000.


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)