vstd
In vstd::
seq
Macros
seq
Structs
Seq
Functions
axiom_seq_add_index1
axiom_seq_add_index2
axiom_seq_add_len
axiom_seq_empty
axiom_seq_ext_equal
axiom_seq_ext_equal_deep
axiom_seq_index_decreases
axiom_seq_len_decreases
axiom_seq_new_index
axiom_seq_new_len
axiom_seq_push_index_different
axiom_seq_push_index_same
axiom_seq_push_len
axiom_seq_subrange_decreases
axiom_seq_subrange_index
axiom_seq_subrange_len
axiom_seq_update_different
axiom_seq_update_len
axiom_seq_update_same
group_seq_axioms
vstd
::
seq
Function
axiom_seq_empty
Copy item path
Settings
Help
Summary
Source
pub
broadcast proof
fn axiom_seq_empty<A>()
Expand description
ensures
#[trigger]
Seq::<A>::empty().len() ==
0
,