GitLab

Allow to give names to the pre/post-conditions, for example using the syntax :

requires arg_pos { x > 0 }

This would be helpful because :

• it would make it clear where this axiom comes from when proving VCs
• it would make the proof more robust as the axiom name would not change from H12 to H13 when adding another requires