Фигурная скобка в дженериках Coq

Question

Следующий код выдает ошибку:

Inductive mylist {A : Set} : Set :=
| mylist_Nil
| mylist_Cons : A -> mylist A -> mylist A.

Ошибка «mylist A» типа «Set» не может быть применена к термину «A»: «Set».Если я изменю «{A: Set}» на (A: Set), тогда он будет работать нормально.

Что означают фигурные скобки?Спасибо!

Answer 1

Обычно аргументы объявляются в скобках.Фигурные скобки используются для неявных аргументов.Неявные аргументы не передаются функциям и объявлениям типов, как обычные;вместо этого средство проверки типов Coq пытается выяснить, какими они должны быть из контекста.

Вы можете принудительно заставить константу явно принимать все аргументы со знаком @, например: @mylist A.

Для универсальных типов, таких как mylist, для Coq недостаточно контекста, чтобы определить, каким должен быть параметр A, поэтому обычно лучше явно объявить эти параметры в скобках.

Руководство пользователя Coq содержит больше информации о неявных аргументах.