Notification Bot (Nov 13 2020 at 12:08): Notification Bot (Nov 13 2020 at 12:08):This topic was moved by Théo Zimmermann to #math-comp users > Finite Types & Finite Graphs in MathComp
Jinoh Kang (Jun 06 2023 at 08:19):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)?
Jinoh Kang (Jun 06 2023 at 08:21):(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)
Jinoh Kang (Jun 06 2023 at 08:24):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
Paolo Giarrusso (Jun 06 2023 at 09:51):From skimming the library as an outsider, induction on the length n + tuple0 and tupleP seem a candidate
Notification Bot (Jun 06 2023 at 11:43):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