Macros§
- assert_
seqs_ equal - Prove two sequences
s1ands2are equal by proving that their elements are equal at each index.
Functions§
- commutative_
foldl - commutative_
foldr - group_
filter_ ensures - group_
seq_ lib_ default - group_
seq_ properties - group_
to_ multiset_ ensures - lemma_
append_ last - lemma_
concat_ associative - lemma_
exactly_ one_ view - lemma_
filter_ view_ commute - lemma_
flatten_ alt_ concat - lemma_
flatten_ concat - lemma_
fold_ left_ permutation - lemma_
fold_ right_ permutation - lemma_
max_ of_ concat - lemma_
min_ of_ concat - lemma_
multiset_ commutative - lemma_
no_ dup_ in_ concat - lemma_
seq_ append_ take_ skip - lemma_
seq_ concat_ contains_ all_ elements - lemma_
seq_ contains - lemma_
seq_ contains_ after_ push - lemma_
seq_ empty_ contains_ nothing - lemma_
seq_ empty_ equality - lemma_
seq_ properties Deprecated - lemma_
seq_ skip_ build_ commut - lemma_
seq_ skip_ contains - lemma_
seq_ skip_ index - lemma_
seq_ skip_ index2 - lemma_
seq_ skip_ len - lemma_
seq_ skip_ nothing - lemma_
seq_ skip_ of_ skip - lemma_
seq_ skip_ update_ commut1 - lemma_
seq_ skip_ update_ commut2 - lemma_
seq_ subrange_ elements - lemma_
seq_ take_ contains - lemma_
seq_ take_ index - lemma_
seq_ take_ len - lemma_
seq_ take_ nothing - lemma_
seq_ take_ update_ commut1 - lemma_
seq_ take_ update_ commut2 - lemma_
seq_ union_ to_ multiset_ commutative - lemma_
sorted_ unique - lemma_
update_ is_ remove_ insert - seq_
to_ set_ distributes_ over_ add - seq_
to_ set_ is_ finite - subrange_
of_ matching_ take - to_
multiset_ build - to_
multiset_ contains - to_
multiset_ insert - to_
multiset_ len - to_
multiset_ remove - to_
multiset_ update