какой тип здесь

Question

Я нашел этот код

Lemma foldlP T S f (s : seq T) x0 (I : nat -> S -> Prop) : 
I 0%N x0 -> 
(forall i x a, (i < size s)%N -> I i x -> I i.+1 (f x (nth a s i))) -> 
I (size s) (foldl f x0 s).

здесь и пытаюсь понять, как он работает. Я думаю, что у меня есть общее представление, но я не могу понять, к какому типу относится переменная a или, собственно, для какой цели она служит аргументом для nth. Я не могу запустить код на своей собственной IDE, так как я искал библиотеку Seq в coq и не нашел ее. Исходя из моего общего понимания только последовательностей, я понятия не имею, какую информацию несет a.

Спасибо!

Answer 1

Переменная a имеет тип T. Его целью является предоставление элемента по умолчанию для функции nth, когда он применяется к пустой последовательности s.

Для запуска этого кода (который доступен на GitHub ), вам нужно установить некоторые библиотеки математических компонентов. Я считаю, что вам просто нужно следующее:

opam install coq-mathcomp-ssreflect
opam install coq-mathcomp-algebra