Is it possible in why3 to make theorems about functions directly? It seems that if I refer to the name of a function in a theorem it says that it is unbound. I have to make a relation using inductive that does the same thing, prove that the function ensures the relation, and then prove that the relation has the desired property.
julia _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
