spaceloop (Mar 18 2021 at 15:04): spaceloop (Mar 18 2021 at 15:04):Is there a way to specify that I don't care about some values of specific indices of an Inductive type? e.g. something along the lines of:
Inductive A (a : Type) : list a -> list a -> Type :=
| C : A (_ :: _) (_ :: _)
I am aware of Generalizable vernacular which saves me the explicit binding, but I still have to come up with (unique) variable names.
Enrico Tassi (Mar 18 2021 at 15:28):No, but what you ask for is a bit risky. In the sense that the order of arguments may matter later on, if you get an heuristic chose for you... you may be surprised.
spaceloop (Mar 18 2021 at 16:52):Do you mean the arguments of C? I don't understand the risk you mean, could you give an example of a heuristic? I am only really interested in relating two terms that have a similar shape, but can have arbitrary (different) subterms.
Paolo Giarrusso (Mar 18 2021 at 19:46):@spaceloop are you asking for how to do it at all, or a shortcut?
Paolo Giarrusso (Mar 18 2021 at 19:47):ah, the latter. Still, I think I see what Enrico means.
Paolo Giarrusso (Mar 18 2021 at 19:48):the expansion could be C a as a’ as’ : A (a :: as) (a’ :: as’), or it could take the arguments in another order — especially if C must take extra arguments than don’t match the underscores you wrote?
Gaëtan Gilbert (Mar 18 2021 at 20:53):the hole for the type (hidden by the :: notation) needs to be filled by a, not a fresh name
sounds like a complicated spec
Last updated: Sep 23 2023 at 14:01 UTC