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)