Commit 2023-01-16 20:04 91288e35

feat(data/fin/tuple): rename fin.append to matrix.vec_append, introduce a new fin.append and fin.repeat. (#10346) We already had fin.append v w h, which combines the append operation with casting. This commit removes the h argument, allowing it to be defeq to fin.add_cases, and moves the previous definition to the name matrix.vec_append matching matrix.vec_cons and similar. Another advantage of dropping h is that it is clearer how to state lemmas like append_assoc, as we only have one proof argument to keep track of instead of four. As it turns out, to implement a gmonoid structure on tuples (under concatenation), fin.append without the h argument is all that's needed. We implement matrix.vec_append in terms of fin.append, but provide a lemma that unfolds it to the old definition so as to avoid having to rewrite all the other proofs. Removing matrix.vec_append entirely is left to investigate in some future PR.