Skip to main content

Module panic

vstd_extra

Module panic 

Source
Expand description

Runtime panic helper whose type (-> !) lets Verus discharge post-conditions by branch elimination at the call site.

Functionsยง

panic_diverge