> Note that an expression such as <" <" A B C "> <" D E F "> <" G H I "> "> > has the type (0..^N) -> ((0..^N) -> R), which would have to be converted > anyway to match the expected I x I -> R type used by square matrices. If we > take I to be (0..^N) then this is just an uncurry, but if the official > index set for matrices is instead (1...N) then the index remapping could be > performed at the same time. > >
The best to do is redefine the <" ...>" operator so that it takes (1 ... N) as its set of indices and then fix up all the proofs referring to the definition. You should have only one definition for matrices, tuples and words since all that is the same story. Or at most two: one with a abstract finite set of indices and another one with (1... N). -- 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/c4106bf2-418a-4b3e-9dae-2d5664c86dddn%40googlegroups.com.
