>This goes back to pop! ; it would seem that push/pop is an abstract >logical idea and shouldn't be specialized with different versions for >each domain/catagory. I might like to temporarily push/pop one of the >elements of the above, infinite, Euclidean domains during calculations >for GCD and not have to rewrite push/pop with all the hazards that >carries. In addition I would have to rely on some abstract >delineation to prove that my new code was "correct". So the abstract >idea and proof has to be abstract and domain free to be coherent.
You're correct that a full proof should be abstract and domain free. But while proving the general case might be possible, a proof might only be available for a specific function in a specific domain. The generalization suggested last time was to add an "assuming" clause, of the form, )abbrev category FOO Foo Foo: Category == Bar with sig1 sig2 == add sig1 == ... assuming AssociativeAxiom: CommuativeAxiom: Proviso1: Definition1: However, within a domain a single function might be easily proven. It might make sense to extend the syntax of == definitions to admit a proof clause, e.g. fn(a:Integer,b:Integer) == someop(a,b) proof: ... Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer