COQ is being used as the proof engine for Spad-level code. The latest change will automatically extract literate chunks labelled 'coq' into a separate location for the COQ proof engine. This can be controlled from the make command line by adding COQ=coq.
ACL2, with its lisp-based syntax and semantics, is the appropriate engine for proving the interpreter and compiler. COQ, with its ability to form dependent types, is the appropriate engine for proving the algebra. Thus we're able to use the best tool for each level of abstraction. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
