| DEFABBREV : THE Solution(s) |
 |
- JEM1 model uses conditional definitions
- ACL2 : wrapper macros simply return argument
- Guard proofs are performed initially
- GCL : type wrappers declare argument
- Obviously introduces configuration issues
- DEFABBREV'ing macros containing type declarations would
- Control expansion and case splitting
- Allow simple rewrite elimination of type terms
|
|
|
|
