Что означает (a: b) c и [a: b] c в некоторых теориях Coq и где оно определено?

Question

Я видел очень странный синтаксис: (name: type1) type2 в типе и [name: type] expr в выражениях, выглядит как альтернативный синтаксис для Pi и Lambda, но я ничего не нашел в документации через несколько часовпоиска, все напрасно.

Что это значит и где оно определено?(Извините, я потерял ссылку на пример использования)

Answer 1

Вы читали теорию, написанную для более старой версии Coq.Синтаксис получил серьезную переработку с V8.0V8.0 поставляется с инструментом для перевода теорий V7 в V8, который работал довольно хорошо;инструмент был удален из последующих выпусков.

Вы можете увидеть обзор изменений в документе Перевод с Coq V7 на V8 .

В частности, (a:b) c - этоуниверсальное количественное определение, теперь написанное forall a:b, c[a:b] c - это лямбда-абстракция, теперь написанная fun a:b => c.Еще одна важная вещь при чтении старых теорий заключается в том, что приложение функции требует скобок и имеет низкий приоритет: до V7 (f x = y) означало (f (x=y)) и ([x:nat]y z) означало (([x:nat]y) z).