I've collected all of the functions that are implemented at the category level. For each function I've prepended the signature. These chunks are automatically extracted during build and collected into a file in the obj/sys/proofs subdirectory. The file has been uploaded to http://daly.axiom-developer.org/coq.v
The file consists of a single COQ Module named Jenks. Each category and its asssociated functions are comments in the file. The categories in the file are arranged so that more primitive categories occur before categories that inherit from them. The next stage is to begin proving these algorithms correct using COQ. Each proven function will be uncommented, along with its associated proof. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer