One implication of the difference is copilot. Copilot can be quite good at figuring out the exact precondition code when given the human prompt. But the way copilot works means that the string would have to be written first. So the latter format would be preferred.
zenna
commented
2 years ago
Currently, the format is:
@pre f(x) = x > 0 "x should be positive"Alternatives are:
"x should be positive" @pre f(x) = x > 0One implication of the difference is copilot. Copilot can be quite good at figuring out the exact precondition code when given the human prompt. But the way copilot works means that the string would have to be written first. So the latter format would be preferred.