Commit 2024-07-16 18:44 3cdee7b8

View on Github →

chore(Data/Stream/Init): use ℕ instead of Nat consistently (#14521) The file currently uses a mix of these: use the nice unicode character, since we can.

Estimated changes

modified def Stream'.drop
modified def Stream'.nats
modified theorem Stream'.append_take_drop
modified theorem Stream'.drop_const
modified theorem Stream'.drop_drop
modified theorem Stream'.drop_map
modified theorem Stream'.drop_succ
modified theorem Stream'.drop_zip
modified theorem Stream'.get?_take_succ
modified theorem Stream'.get_const
modified theorem Stream'.get_drop
modified theorem Stream'.get_even
modified theorem Stream'.get_inits
modified theorem Stream'.get_interleave_left
modified theorem Stream'.get_map
modified theorem Stream'.get_nats
modified theorem Stream'.get_odd
modified theorem Stream'.get_succ
modified theorem Stream'.get_succ_cons
modified theorem Stream'.get_succ_iterate'
modified theorem Stream'.get_succ_iterate
modified theorem Stream'.get_tails
modified theorem Stream'.get_zip
modified theorem Stream'.mem_of_get_eq
modified theorem Stream'.tail_drop
modified theorem Stream'.take_succ
modified theorem Stream'.take_theorem