bend-mathlib

Search uses release 0.8.1.0 · 1,126 definitions

Releases (15)

0.8.1.0 indexed
0.8.0.0 unindexed
0.7.5.0 unindexed
0.7.4.0 unindexed
0.7.3.0 unindexed
0.7.2.0 unindexed
0.7.1.0 unindexed
0.7.0.0 unindexed
0.6.0.0 unindexed
0.5.0.0 unindexed
0.4.0.0 unindexed
0.3.0.0 unindexed
0.2.0.0 unindexed
0.1.0.1 unindexed
0.1.0.0 unindexed

Definitions (1,126)

sort.bend

def internal_sorted_tail
def internal_le_flip_nat
def internal_le_trans_nat
def internal_cons_ins_step
def internal_sorted_cons_ins
def internal_insert_step
def insert_by_sortedInserting into a sorted list keeps it sorted, for a total comparator.
def isort_by_sortedInsertion sort returns a sorted list.
def isort_by_sorted_natInsertion sort returns a sorted Nat list.
def internal_all_geA recursion, not List.all with a lambda over lo, which --verdict cannot translate (PLAN F38).
def internal_least
def internal_least_intro
def internal_least_cons_le
def internal_least_cons_tail
def internal_least_trans
def internal_sorted_least_head
def internal_sorted_cons_of_least
def internal_least_merge_pick
def internal_least_merge
def internal_merge_sorted_pick
def merge_by_sortedMerging two sorted lists is sorted (needs transitivity, and totality for the un-taken branch).
def merge_by_sorted_natMerging two sorted Nat lists gives a sorted list.
def internal_length_zero
def internal_sorted_short
def internal_length_evens_le
def internal_length_odds_le
def msort_by_sortedMerge sort returns a sorted list once the fuel reaches the input length (invariant: length <= fuel+1).
def sort_by_sortedMerge sort of the full-length fuel sorts its input.
def msort_by_sorted_natMerge sort with fuel = length returns a sorted Nat list (h always holds; sort_by_sorted_nat needs no h).
def sort_by_sorted_natMerge sort returns a sorted Nat list.

string.bend

def internal_false_ne_true
def internal_append_nil
law append_nilThe empty string is a right identity for append: a ++ "" = a.
law nil_appendThe empty string is a left identity for append: "" ++ a = a.
def internal_append_assoc
law append_assocAppend is associative: (a ++ b) ++ c = a ++ (b ++ c).
def internal_length_append
law length_appendThe length of an append is the sum of the lengths.
def internal_reverse_go_spec
law reverse_go_specThe reverse accumulator loop appends the reversed string to the accumulator.
def internal_reverse_append
law reverse_appendReversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a.
def internal_reverse_reverse
law reverse_reverseReversing twice gives the string back.
def internal_word_cmp_refl
def internal_u32_cmp_refl
law u32_cmp_reflComparing a U32 with itself gives EQ.
def internal_char_cmp_refl
law char_cmp_reflComparing a character with itself gives EQ and hands both back.
def internal_cmp_refl
law cmp_reflComparing a string with itself gives EQ and hands both back.
def internal_order_go_ltBase 2.0.38 defines String.order directly, not through String.cmp (PLAN F39); these prove the two agree.
def internal_order_go_gt
def internal_cmp_rec_snd
def internal_order_step
def internal_order_cmp_go
def internal_order_cmpProofs about String.eq unfold String.order only through this.
def internal_eq_true_cmp
def internal_cmp_true_eq
law eq_reflEvery string is equal to itself under String.eq.
def internal_fin_head
def internal_fin_tail
def internal_word_eq
law u32_eq_of_is_eqTwo U32s that U32.is_eq calls equal are equal.
law char_eq_of_is_eqTwo characters that Char.is_eq calls equal are equal.
def internal_rec_is_eq
def internal_is_eq_of
def internal_step
law eq_of_eq_trueTwo strings that String.eq calls equal are equal.
def internal_length_reverse_go
law length_reverseReversing preserves the length.
law reverse_nilReversing the empty string gives the empty string.
law reverse_singletonReversing a one-character string gives it back.
law is_empty_iff_length_eq_zeroA string is empty exactly when its length is zero.
law is_empty_appendAn append is empty exactly when both parts are.
def internal_is_empty_reverse_go
law is_empty_reverseThe reverse is empty exactly when the string is.
law take_append_dropTaking n characters and appending the rest after dropping n gives the string back.
law length_takeTaking n characters leaves min(n, length) of them.
law length_dropDropping n characters leaves length - n of them.
law to_list_from_listConverting a character list to a string and back gives the list.
law from_list_to_listConverting a string to a character list and back gives the string.
law to_list_appendThe characters of an append are the characters of each part, appended.
law length_to_listA string has as many characters as its character list.
law append_nil_symThe empty string is a right identity for append: a ++ "" = a, reversed to rewrite toward the simple side.
law nil_append_symThe empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.
law append_assoc_symAppend is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.
law length_append_symThe length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
law reverse_go_spec_symThe reverse accumulator loop appends the reversed string to the accumulator, reversed to rewrite toward the simple side.
law reverse_append_symReversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a, reversed to rewrite toward the simple side.
law reverse_reverse_symReversing twice gives the string back, reversed to rewrite toward the simple side.
law u32_cmp_refl_symComparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.
law char_cmp_refl_symComparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
law cmp_refl_symComparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
law eq_refl_symEvery string is equal to itself under String.eq, reversed to rewrite toward the simple side.
law length_reverse_symReversing preserves the length, reversed to rewrite toward the simple side.
law reverse_nil_symReversing the empty string gives the empty string, reversed to rewrite toward the simple side.
law reverse_singleton_symReversing a one-character string gives it back, reversed to rewrite toward the simple side.
law is_empty_iff_length_eq_zero_symA string is empty exactly when its length is zero, reversed to rewrite toward the simple side.
law is_empty_append_symAn append is empty exactly when both parts are, reversed to rewrite toward the simple side.