Type annotations in definitions
Type annotations make code more readable to developers. I wonder if it would be good to set a directive in Prosa to have type annotations for all definition arguments and returns types. It would be particularly useful to differentiate between computable (return type bool
) and noncomputable definitions (return type : pred
) at a glance.