Commit 2023-05-17 12:05 f513eb6d

View on Github →

chore: bump dependencies (#4012) This just bumps the Std dependency, to get access to Mario's new "Try this:" implementation.

Estimated changes

deleted theorem String.csize_pos
deleted theorem List.drop_sublist
deleted theorem List.drop_subset
deleted theorem List.drop_suffix
deleted theorem List.eq_nil_of_infix_nil
deleted theorem List.infix_append'
deleted theorem List.infix_append
deleted theorem List.infix_concat
deleted theorem List.infix_cons
deleted theorem List.infix_cons_iff
deleted theorem List.infix_nil_iff
deleted theorem List.infix_of_mem_join
deleted theorem List.infix_refl
deleted theorem List.isInfix.filter
deleted theorem List.isInfix.length_le
deleted theorem List.isInfix.trans
deleted theorem List.isPrefix.filter
deleted theorem List.isPrefix.isInfix
deleted theorem List.isPrefix.length_le
deleted theorem List.isPrefix.trans
deleted theorem List.isSuffix.filter
deleted theorem List.isSuffix.isInfix
deleted theorem List.isSuffix.length_le
deleted theorem List.isSuffix.trans
deleted theorem List.mem_of_mem_take
deleted theorem List.nil_infix
deleted theorem List.nil_prefix
deleted theorem List.nil_suffix
deleted theorem List.prefix_append
deleted theorem List.prefix_cons_inj
deleted theorem List.prefix_nil_iff
deleted theorem List.prefix_refl
deleted theorem List.reverse_infix
deleted theorem List.reverse_prefix
deleted theorem List.reverse_suffix
deleted theorem List.suffix_append
deleted theorem List.suffix_cons
deleted theorem List.suffix_cons_iff
deleted theorem List.suffix_nil_iff
deleted theorem List.suffix_refl
deleted theorem List.take_prefix
deleted theorem List.take_sublist
deleted theorem List.take_subset
deleted theorem Nat.add_pos_left
deleted theorem Nat.add_pos_right
deleted theorem String.get.cons_add_csize
added theorem String.length_data
deleted theorem String.length_toList
deleted theorem String.ltb.cons_add_csize
deleted theorem String.popn_empty
modified theorem String.toList_nonempty
deleted theorem String.toList_singleton
deleted def String.popn
modified def addHaveSuggestion
deleted def addRefineSuggestion
modified def addRewriteSuggestion