Wouldn’t they be clearly differentiated in a type theory setup? How does coq/lean treat those? Are they the same concept or separated ones?
-stan On Wed, Sep 2, 2020 at 8:51 PM 'fl' via Metamath <[email protected]> wrote: > > > > > I do not like the idea to regard words as vectors - these are two > completely different concepts > > > > > Simply do a computer program and you will realize soon that tuples can be > concatenated at will. > Length is a concept relevant to words and matrices. > > There is an abstract theory of words regarding them as elements of free > structures. Concatenation is > not at all an operation of its own. It's an operation similar to the > others. > > Pretty sure that some transformation of matrices can be analyzed in terms > of concatenation or subwords. > > No definitely it's the same concept. > > -- > FL > > > > > > > > > -- > > > You received this message because you are subscribed to the Google Groups > "Metamath" group. > > > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > > > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/004ddf15-75e7-4bcb-90ec-94b021bfe12fn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/004ddf15-75e7-4bcb-90ec-94b021bfe12fn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0wnkT5GnnRE7BuQKtuj0BTc5QWvGjQTotmKHTAE4t48fQ%40mail.gmail.com.
