vstd
In vstd::
pervasive
Macros
struct_with_invariants
Traits
FnWithRequiresEnsures
ForLoopGhostIterator
ForLoopGhostIteratorNew
VecAdditionalExecFns
Functions
affirm
allow_panic
arbitrary
assert
assume
cloned
print_u64
proof_from_false
runtime_assert
spec_affirm
strictly_cloned
trigger
unreached
vstd
::
pervasive
Function
proof_from_false
Copy item path
Settings
Help
Summary
Source
pub
proof
fn proof_from_false<A>() ->
tracked
a :
A
Expand description
requires
false
,