Commit 2025-01-14 02:01 264ed5bc

View on Github →

feat: add stream' lemmas (#19546) The orders of summands in some lemmas are changed and simp annotations are added to make the API closer to the one for lists.

Estimated changes

added theorem Stream'.append_eq_cons
added theorem Stream'.append_take
modified theorem Stream'.concat_take_get
modified theorem Stream'.corec'_eq
modified theorem Stream'.corec_eq
modified theorem Stream'.drop_drop
modified theorem Stream'.drop_tail'
modified theorem Stream'.eq_of_bisim
modified theorem Stream'.get_drop
modified theorem Stream'.get_of_bisim
modified theorem Stream'.get_succ_cons
added theorem Stream'.map_take
modified theorem Stream'.nil_append_stream
modified theorem Stream'.tail_drop'
added theorem Stream'.take_add
added theorem Stream'.take_drop
added theorem Stream'.take_get
added theorem Stream'.take_prefix
modified theorem Stream'.unfolds_eq