I was wondering, Zeno capable of proving just equational statements, or is it able to prove more general statements about programs? In particular, it would be interesting if Zeno would be able to prove that a function is total by verifying that it uses only structural (inductive) recursion (on a well defined inductive type), i.e. each recursive function call must be on a syntactic subcomponent of its parameter. And dually, one might want to prove that a function is corecursive, meaning that each recursive call is guarded by a constructor.
Best regards, Petr
Yeah as it is Zeno can only prove equality properties, but I would love to extend it with these other proof features. I'm currently working on a more general notion of well-founded ordering within the program (so that it can hopefully verify quicksort/mergesort) and I guess I could expose this feature so one could prove the totality of functions in the way you said. Cheers, Will