This topic was moved by Théo Zimmermann to #math-comp users > Finite Types & Finite Graphs in MathComp
Is there a "best practice" way of induction over tuples, other than defining my own induction principle? Should I just take the seq/list out of it and start from O for (size t)?
(Side note: I admit that it took me a bit to realize that seq ?T is finite, since it's an inductive type, not a coinductive type à la streams)
It appears to me that naïvely destructing the tval leads to impossible goals since e.g., it asserts that [::] is an n.+1-tuple
From skimming the library as an outsider, induction on the length n + tuple0 and tupleP seem a candidate
4 messages were moved from this topic to #math-comp users > Finite Types & Finite Graphs in MathComp by Karl Palmskog.
Last updated: Oct 03 2023 at 04:02 UTC