|
|
|---|
|
|
|
|---|
A beta-reduction routine and associated proof of correctness
This book provides a proof of correctness for a simple beta-reduction routine under a generic ACL2 evaluator. Any user defined ACL2 evaluator should support functional instantiation of this result, allowing this beta reduction routine to be used with any ACL2 evaluator, for example in proving a :meta rule.