Partial Functions in ACL2

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)

Last updated October 2001 manolios@cc.gatech.edu

Back to Pete's home page College of Computing