Через CpdtTactics.v:
CpdtTactics.v
[...] Успешно, если x находится в списке ls, представлен левым вложенным кортежем. Ltac inList x ls := match ls with | x => idtac | (_, x) => idtac | (?LS, _) => inList x LS end.
[...] Успешно, если x находится в списке ls, представлен левым вложенным кортежем.
x
ls
Ltac inList x ls := match ls with | x => idtac | (_, x) => idtac | (?LS, _) => inList x LS end.
Это кажется нетипичным.Разве хвост списка обычно не входит в правую часть кортежа?
Каким-то образом n-кортежи - это вложенные пары, связанные слева:
(x, y, z)
десугары в
pair (pair x y) z
И это то, что мы получаем, если хотим написать inList x (x, y, z).
inList x (x, y, z)
Через личное общение с Адамом:
Нет, на самом деле я не могу придумать способ отдать одну версию другой.Мне просто нужно было сделать какой-то выбор для этой части книги.