def function transparency principle


We generally want to encourage the use of def functions, rather than macros. Def functions provide better diagnostic for failed verifications, provide useful hooks for triggering, for providing additional contract information, and could someday provide more flexible control for deduction. However, to achieve these benefits, we need simple ways to make def functions transparent by default, in the sense that using a def rather than a macro should never (or very rarely) cause a verification to fail. That is not presently the case.