CODEWITHSUNDEEP
coq
Federico
Federico

Reputation: 2133

Why, in Coq, a record projection expects a Type as argument?

I would like to formalize a data structure (a string concatenation) in 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)
}.

However, I get an error in the last record:

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

Why does it expect a Type? The projection seed should take a SeedPassword A, right?

Upvotes: 0

Views: 131

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

About seed.

returns:

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

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

So, seed needs the type, otherwise A in SeedPassword A will be unbounded.

You can solve the issue with implicit arguments, which Coq will try to infer. One way to do it is to put

Set Implicit Arguments.

into your file (usually after the imports). Or you can use Arguments command like so:

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

Upvotes: 1

Related Questions