assert #

Syntax #

V@[assert] ::= assert (V@[spec_expr]) ;

Proof operation #

Prove the given expression using the default solver, and then assume the predicate for subsequent code.