Giving names to requires and ensures
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
toH13
when adding anotherrequires
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information