Martin, I like the idea of "specific mathematical axiom markup" as a first cut. I will try this idea.
This is (reasonably) easy to do as there are already some markers in place. These are the "attributes" such as LeftUnitary. Unfortunately most of them are somewhat more advanced, such as FiniteAggregate, which requires the use of dependent types. That's still a steep hill to climb. Axiom has signatures already. The real hack would be to unify the signatures used by COQ with the signatures used by Axiom. That way COQ would have access to the Axiom signature database and Axiom would be able to use COQ to prove Spad code. This would be the very essence of elegance. Right now in Axiom you can say )d op pop! and it will show you signatures and examples from domains. Perhaps we can develop a "rewriter" that will translate the Axiom signature to a COQ signature. ========================================================== )d op pop! There are 4 exposed functions called pop! : [1] ArrayStack(D1) -> D1 from ArrayStack(D1) if D1 has SETCAT [2] Dequeue(D1) -> D1 from Dequeue(D1) if D1 has SETCAT [3] D -> D1 from D if D has SKAGG(D1) and D1 has TYPE [4] Stack(D1) -> D1 from Stack(D1) if D1 has SETCAT Examples of pop! from ArrayStack a:ArrayStack INT:= arrayStack [1,2,3,4,5] pop! a a Examples of pop! from Dequeue a:Dequeue INT:= dequeue [1,2,3,4,5] pop! a a Examples of pop! from StackAggregate a:Stack INT:= stack [1,2,3,4,5] pop! a a Examples of pop! from Stack a:Stack INT:= stack [1,2,3,4,5] pop! a a ============================================================= There really ought to be a way to show the mathematical axioms, possibly as part of the output of the )show command. Tim _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
