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.
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.
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.
@spaceloop are you asking for how to do it at all, or a shortcut?
ah, the latter. Still, I think I see what Enrico means.
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?
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