|
|
|---|
|
|
|
|---|
Enable Defdata aliasing
Defdata will try and determine if proposed data definitions are equivalent to existing data definitions and if so, Defdata will create alias types. The advantage is that any existing theorems can be used to reason about the new type. Defdata will generate macros for the recognizers and enumerators, which means that during proofs, you will see the recognizer for the base type. If you turn this off, then you can still use defdata-alias to explicitly tell ACL2s to alias types.
Usage: (acl2s-defaults :get defdata-aliasing-enabled) (acl2s-defaults :set defdata-aliasing-enabled t) :doc defdata-aliasing-enabled