There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
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.