e.g. we might want to do something like let x = (some complex expression) and then use x in several different preconditions. This allows us to avoid repeating the complex expression.
assert is useful in case the solver needs some help showing that the preconditions and/or postconditions are well-defined. Same for hide and show.
There may also be some value in allowing to call "lemma" functions within pre/postcondition blocks. Maybe ghost lemma_name(x,y,z); could be used here.
e.g. we might want to do something like
let x = (some complex expression)and then usexin several different preconditions. This allows us to avoid repeating the complex expression.assertis useful in case the solver needs some help showing that the preconditions and/or postconditions are well-defined. Same forhideandshow.There may also be some value in allowing to call "lemma" functions within pre/postcondition blocks. Maybe
ghost lemma_name(x,y,z);could be used here.