guard
is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. decide
is a lot more common, and so people are more likely to know how to deal with it.
guard
is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. decide
is a lot more common, and so people are more likely to know how to deal with it.