Я получаю ошибку типа в последней строке следующей программы:
Require Import List.
Import ListNotations.
(* This computes to 10 *)
Compute (fold_right plus 0 [1;2;3;4]).
(* I want this to compute to [5;6;7;8] but it gives a type error instead *)
Compute (fold_right app [] [[5;6]; [7;8]]).
Это ошибка, которую я получаю:
Error:
The term "app" has type "forall A : Type, list A -> list A -> list A" while it is expected to have type
"Type -> ?A -> ?A" (cannot instantiate "?A" because "A" is not in its scope).
Я действительно не понимаю, почему я получаю эту ошибку. Чем здесь отличаются app и plus? Связано ли это с тем, что app полиморфна, а plus является мономорфной nat -> nat -> nat функцией?
Если это имеет значение, моя версия Coq — 8.5.
