Почему в Coq проекция записи ожидает тип в качестве аргумента? - PullRequest
Новая
       4

Почему в Coq проекция записи ожидает тип в качестве аргумента?

0 голосов
/ 25 июня 2018

Я хотел бы формализовать структуру данных (конкатенацию строк) в Coq: 

Require Import List.

Record SeedPassword (A: Type): Type := {
    seed: list A;
    password: list A
}.

Record SeedPasswordConcatenation {A: Type} (S: SeedPassword A): Type := {
    concatenation: list A;
    proof: concatenation = (seed S ++ password S)
}.

Однако я получаю сообщение об ошибке в последней записи: 

The term "S" has type "SeedPassword A" while it is expected to have type "Type".

Почемуэто ожидать Type?Проекция seed должна занять SeedPassword A, верно?

1 Ответ

0 голосов
/ 25 июня 2018 
About seed.

возвращает: 

seed : forall A : Type, SeedPassword A -> list A

Argument scopes are [type_scope _]
seed is transparent
Expands to: Constant Top.seed

Таким образом, seed нужен тип, в противном случае A в SeedPassword A будет неограниченным.

Вы можете решить проблему с неявными аргументами, которые Coq попытается вывести.Один из способов сделать это - поместить 

Set Implicit Arguments.

в ваш файл (обычно после импорта).Или вы можете использовать команду Arguments следующим образом: 

Record SeedPassword (A: Type): Type := {
    seed: list A;
    password: list A
}.
Arguments seed {A} _.
Arguments password {A} _.
...