Le 02/10/2019 à 15:16, Julia Lawall a écrit : > Is there any advantage to not making a lemma a lemma function?
Apart from concerns about name pollution and performances, I cannot see any right now. > Hmm, in looking further, I have the impression that I can't make a let > lemma because the lemma needs to be universally quantified over some > variables. If the quantified variables are always the same, you can move them from the arguments to the postcondition of the lemma function. You could also prove the lemma once and for all, and then prove multiple trivial variants of it as lemma functions, so that they can be instantiated differently depending on your use cases. I agree that none of those solutions are especially elegant. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
